package heraclito;

import java.io.*;
import java.awt.Color;
import java.awt.Font;
import java.util.ArrayList;
import java.util.Calendar;
import java.util.logging.Level;
import java.util.logging.Logger;
import javax.swing.JFileChooser;
import javax.swing.JOptionPane;
import javax.swing.filechooser.FileNameExtensionFilter;
import logic.Formula;
import logic.ParserException;
import logic.ScannerException;
import org.jdesktop.application.Action;

public class Edicao extends javax.swing.JPanel {

    public static final int PROPOSITION = 1,
            PARENTHESIS = 2,
            NEGATION = 3,
            CONJUNCTION = 4,
            DISJUNCTION = 5,
            CONDITIONAL = 6,
            BICONDITIONAL = 7;
    
    private static final String regras[] = {"MP","AD","CJ","IEQ","EEQ","SP","EDJ","PC","RAA",
        "DN","MT","SH","SD","INC","DC","EXP"};
    private Linha Teorema[]; //Teorema original
    private Linha TeoremaAux[]; //Teorema auxiliar que controla Desfazer/Refazer
    private Formula hipoteses[];
    private int indiceoriginal = 0; //Tamanho máximo do teorema
    private int indice = 0; //Controla a posição do teorema no Desfazer e Refazer
    private int pos1 = 0; //Variaveis que controlam a seleção das opções para as regras
    private int pos2 = 0; //Variaveis que controlam a seleção das opções para as regras
    private int pos3 = 0; //Variaveis que controlam a seleção das opções para as regras
    private int total_hipoteses = 0;//Variavel que controla a ação de desfazer
    private boolean carregar = false;
    private int lastbtn = 0;// indica a ultima regra utilizada
    private int opcao = 0;
    private int qtPCRAA = 0;//indica quantos '|' colocar
    private String resPCRAA[];//indica qual a fórmula a ser derivada das regras PC e RAA, e também qual das duas regras foi a ultima utilizada
    private ArrayList msgAgent;
    private boolean regraCorreta;
    private String nivel;
    private HeraclitoView Principal;
    private String argumentoFormatado;
    private int qtAjuda;
    private int qtErrosRegras[];
    private int qtErrosSeguidos;
    private String resolucao[];//Resolução recebida do servidor

    public Edicao(HeraclitoView Principal) {
        initComponents();

        //Declaração provisória
        Teorema = new Linha[100];
        resPCRAA = new String[50];
        this.Principal = Principal;
        msgAgent = new ArrayList();
        regraCorreta = false;
        setComboBox2();
        //btnIniciar.setEnabled(false);
        jComboBox1.setEnabled(false);
        btnRefazer.setEnabled(false);
        btnDesfazer.setEnabled(false);
//        txtArgumento.setVisible(true);//CORRIGIR PARA PRÓXIMA VERSÃO
//        btnIniciar.setVisible(true);//***************
//        btnIniciar.setEnabled(true);//*************8
//        jComboBox2.setVisible(false);//**************8
        txtArgumento.setVisible(false);
        btnIniciar.setVisible(false);
        btnIniciar.setEnabled(false);
        jComboBox1.setVisible(false);
        jComboBox2.setVisible(true);
        //btnIniciar.setVisible(false);
        setBotoes(false, false, false);
        informaLogado();
        qtErrosRegras = new int[16];
        jSplitPane1.remove(2);
        
        ajudaDica.setVisible(false);//Mudar quando existir possibilidade de ajuda do servidor.
    }

    private void setComboBox2() {
        jComboBox2.addItem("Inserir argumento");
        jComboBox2.addItem("Básico");
        jComboBox2.addItem("Intermediário");
        jComboBox2.addItem("Avançado");
        jComboBox2.addItem("Lista_de_exercícios");
    }

    private void alteraCor() {
        btnMP.setBackground(pnlRegras.getBackground());
        btnAD.setBackground(pnlRegras.getBackground());
        btnCJ.setBackground(pnlRegras.getBackground());
        btnEEQ.setBackground(pnlRegras.getBackground());
        btnIEQ.setBackground(pnlRegras.getBackground());
        btnDN.setBackground(pnlRegras.getBackground());
        btnPC.setBackground(pnlRegras.getBackground());
        btnRAA.setBackground(pnlRegras.getBackground());
        btnSP.setBackground(pnlRegras.getBackground());
        btnEDJ.setBackground(pnlRegras.getBackground());
        btnMT.setBackground(pnlRegras.getBackground());
        btnINC.setBackground(pnlRegras.getBackground());
        btnEXP.setBackground(pnlRegras.getBackground());
        btnSD.setBackground(pnlRegras.getBackground());
        btnSH.setBackground(pnlRegras.getBackground());
        btnDC.setBackground(pnlRegras.getBackground());
    }

    @Action
    public void Desfazer() {
        if (indice > total_hipoteses) { //Se não for o início do teorema pode Desfazer

            indice--; //Atualizar variavel auxiliar de controle

            for (int i = 0; i <= indice; i++) { //Carrega o teorema principal com os dados do teorema auxiliar, com base no indice auxiliar
                Teorema[i] = TeoremaAux[i];
            }

            Teorema[indice + 1] = null; //Limpa a última posição do teorema

            if (qtPCRAA < Teorema[indice].getQtPCRAA()) {
                ReativaPCRAA();
            }
            qtPCRAA = Teorema[indice].getQtPCRAA();
            lstTeorema.clearSelection(); //Limpa lista
            lstTeorema.setListData(Teorema); //Carrega lista com os novos dados do Teorema
            lstTeorema.setEnabled(true);
            btnRefazer.setEnabled(true);
            if (indice == total_hipoteses) {
                btnDesfazer.setEnabled(false);
            }
        }
    }

    @Action
    public void Refazer() {
        if (indiceoriginal > indice) { //Verifica se pode ser refeito com base nas últimas alterações

            indice++;  //Atualizar variavel auxiliar de controle

            for (int i = 0; i <= indice; i++) { //Carrega o teorema principal com os dados do teorema auxiliar, com base no indice auxiliar
                Teorema[i] = TeoremaAux[i];
            }

            qtPCRAA = Teorema[indice].getQtPCRAA();
            lstTeorema.clearSelection(); //Limpa lista
            lstTeorema.setListData(Teorema); //Carrega lista com os novos dados do Teorema]
            btnDesfazer.setEnabled(true);
            if (indiceoriginal == indice) {
                btnRefazer.setEnabled(false);
            }
        }
    }

    private void popup1(String opcao1, String opcao2) {
        jFrame1.setBounds(550 - (opcao1.length()) * 5, 300, (opcao1.length() + opcao2.length()) * 6 + 200, 200);
        btnDireita.setBounds(10, 75, opcao1.length(), 1);
        btnDireita.setText(opcao1);
        btnEsquerda.setBounds(20 + opcao1.length(), 75, opcao2.length(), 1);
        btnEsquerda.setText(opcao2);
        btnAmbos.setBounds(30 + opcao1.length() + opcao2.length(), 75, 10, 1);
        btnAmbos.setText("ambas");
        jFrame1.setVisible(true);
    }

    private void popup2(String opcao1) {
        jFrame2.setBounds(500, 200, 220, 360);
        jButton1.setBounds(10, 75, 100, 1);
        jButton1.setText(opcao1 + " v");
        jButton2.setBounds(20 + opcao1.length(), 75, 100, 1);
        jButton2.setText("v " + opcao1);
        jFrame2.setVisible(true);
    }

    private void popup3() {
        if (lastbtn == 8) {
            jLabel41.setText("Digite a fórmula final que você deseja derivar da regra PC.");
            jLabel42.setText("Por exemplo: a->b");
        } else if (lastbtn == 9) {
            jLabel41.setText("Digite a fórmula que você deseja negar usando a regra RAA.");
            jLabel42.setText("Por exemplo: a para provar ~a.");
        } else if (lastbtn == 14) {
            jLabel41.setText("Digite a fórmula que você deseja derivar da regra INC.");
            jLabel42.setText("Por exemplo: a");
        }
        jFrame3.setBounds(550, 300, 320, 200);
        jFrame3.setVisible(true);
    }

    @Action
    public void btn1() {
        opcao = 1;
        carregar = true;
        if (lastbtn == 2) {
            Regra_AD();
        } else if (lastbtn == 5) {
            Regra_EEQ();
        } else if (lastbtn == 6) {
            Regra_SP();
        }
    }

    @Action
    public void btn2() {
        opcao = 2;
        carregar = true;
        if (lastbtn == 2) {
            Regra_AD();
        } else if (lastbtn == 5) {
            Regra_EEQ();
        } else if (lastbtn == 6) {
            Regra_SP();
        }
    }

    @Action
    public void btn3() {
        opcao = 3;
        carregar = true;
        if (lastbtn == 5) {
            Regra_EEQ();
        } else if (lastbtn == 6) {
            Regra_SP();
        }
    }

    @Action
    public void btnOK() {
        jFrame3.setVisible(false);
        if (lastbtn == 8) {
            Regra_PC();
        } else if (lastbtn == 9) {
            Regra_RAA();
        } else if (lastbtn == 14) {
            aplicaINC();
        }
    }

    @Action
    public void btnCancela() {
        jFrame1.setVisible(false);
        jFrame2.setVisible(false);
        jFrame3.setVisible(false);
        alteraCor();
        carregar = false;
    }

    @Action
    public void Regra_MP() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 1) {
            //Altera cor do botão
            btnMP.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 1;
        } else {

            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0 && pos2 != 0) {
                //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<<)
                Teorema[pos1].unselect();

                //Valida para aplicar a Regra Modus Ponens
                if (Teorema[pos1].getFormula().display().length() < Teorema[pos2].getFormula().display().length() && Teorema[pos2].getFormula().getType() == CONDITIONAL) {
                    if (Teorema[pos2].getFormula().getLeft().equalsTo(Teorema[pos1].getFormula()))//analisa se a regra modus pones pode ser aplicada
                    {
                        Teorema[++indice] = new Linha(Teorema[pos2].getFormula().getRight(), " ", "MP ", qtPCRAA, indice);
                        ajusta();
                    }
                } else if (Teorema[pos1].getFormula().display().length() > Teorema[pos2].getFormula().display().length() && Teorema[pos1].getFormula().getType() == CONDITIONAL) {
                    if (Teorema[pos1].getFormula().getLeft().equalsTo(Teorema[pos2].getFormula())) {
                        Teorema[++indice] = new Linha(Teorema[pos1].getFormula().getRight(), " ", "MP ", qtPCRAA, indice);
                        ajusta();
                    }
                }

                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração
                pos1 = 0;
                pos2 = 0;

                organiza();
                testaRegra();
                confirma();
                //Atualiza variaveis de controle
                carregar = false;
            }
        }
    }

    @Action
    public void Regra_AD() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 2) {
            //Altera cor do botão
            btnAD.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 2;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0) {
                String temp1 = "", temp2 = "";
                //Valida para aplicar a Regra Adição
                if (Teorema[pos1].getFormula().getType() != PROPOSITION
                        && Teorema[pos1].getFormula().getType() != NEGATION
                        && Teorema[pos1].getFormula().getType() != PARENTHESIS) {
                    temp1 = "(" + Teorema[pos1].getFormula().display() + ")";
                } else {
                    temp1 = Teorema[pos1].getFormula().display();
                }
                if (jTextField1.getText().contains("^") || jTextField1.getText().contains("->") || jTextField1.getText().contains("v")) {
                    temp2 += "(" + jTextField1.getText() + ")";
                } else {
                    temp2 += jTextField1.getText();
                }
                popup2(temp1);
                if (temp2.length() > 0) {
                    try {
                        Formula f1 = new Formula();
                        f1.parse(temp2);
                        Formula f2 = new Formula();
                        f2.parse(temp1);
                        if (opcao == 1) {
                            Teorema[++indice] = new Linha(new Formula(DISJUNCTION, f2, f1), " ", "AD ", qtPCRAA, indice);
                            jFrame2.setVisible(false);
                            ajusta();
                            pos1 = 0;
                        } else if (opcao == 2) {
                            Teorema[++indice] = new Linha(new Formula(DISJUNCTION, f1, f2), " ", "AD ", qtPCRAA, indice);
                            jFrame2.setVisible(false);
                            ajusta();
                            pos1 = 0;
                        }
                        testaRegra();
                    } catch (ScannerException ex) {
                        JOptionPane.showMessageDialog(null, "Erro na fórmula.");
                    } catch (ParserException ex) {
                        JOptionPane.showMessageDialog(null, "Erro na fórmula.");
                    }
                }
                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração

                //Atualiza variaveis de controle
                carregar = false;
                opcao = 0;
                jTextField1.setText("");
                organiza();
                confirma();
            }
        }
    }

    @Action
    public void Regra_CJ() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 3) {
            //Altera cor do botão
            btnCJ.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 3;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0 && pos2 != 0) {
                //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<<)
                Teorema[pos1].unselect();
                Teorema[++indice] = new Linha(new Formula(CONJUNCTION, Teorema[pos1].getFormula(), Teorema[pos2].getFormula()), " ", "CJ ", qtPCRAA, indice);
                ajusta();

                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração

                //Atualiza variaveis de controle
                carregar = false;
                pos1 = 0;
                pos2 = 0;
                organiza();
                testaRegra();
                confirma();
            }
        }
    }

    @Action
    public void Regra_IEQ() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 4) {
            //Altera cor do botão
            btnIEQ.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 4;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0 && pos2 != 0) {
                //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<<)
                Teorema[pos1].unselect();

                //Valida para aplicar a Regra Introdução da equivalência
                if(Teorema[pos1].getFormula().hasLeft())
                    if (Teorema[pos1].getFormula().getLeft().equalsTo(Teorema[pos2].getFormula().getRight()) && Teorema[pos2].getFormula().getLeft().equalsTo(Teorema[pos1].getFormula().getRight())) {
                        Formula f = new Formula(BICONDITIONAL, Teorema[pos1].getFormula().getLeft(), Teorema[pos1].getFormula().getRight());
                        Teorema[++indice] = new Linha(f, " ", "+EQ ", qtPCRAA, indice);
                        ajusta();
                    }

                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração


                //Atualiza variaveis de controle
                carregar = false;
                pos1 = 0;
                pos2 = 0;
                organiza();
                testaRegra();
                confirma();
            }
        }
    }

    @Action
    public void Regra_EEQ() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 5) {
            //Altera cor do botão
            btnEEQ.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 5;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0) {
                if (Teorema[pos1].getFormula().getType() == BICONDITIONAL) {
                    regraCorreta = true;
                    //Valida para aplicar a Regra Introdução da equivalência
                    Formula opcao1 = new Formula(CONDITIONAL, Teorema[pos1].getFormula().getLeft(), Teorema[pos1].getFormula().getRight());
                    Formula opcao2 = new Formula(CONDITIONAL, Teorema[pos1].getFormula().getRight(), Teorema[pos1].getFormula().getLeft());
                    if (opcao == 0) {
                        popup1(opcao1.display(), opcao2.display());
                    } else if (opcao == 1) {
                        Teorema[++indice] = new Linha(opcao1, " ", "-EQ ", qtPCRAA, indice);
                        jFrame1.setVisible(false);
                        ajusta();
                        pos1 = 0;
                    } else if (opcao == 2) {
                        Teorema[++indice] = new Linha(opcao2, " ", "-EQ ", qtPCRAA, indice);
                        jFrame1.setVisible(false);
                        ajusta();
                        pos1 = 0;
                    } else if (opcao == 3) {
                        Teorema[++indice] = new Linha(opcao1, " ", "-EQ ", qtPCRAA, indice);
                        ajusta();
                        confirma();
                        Teorema[++indice] = new Linha(opcao2, " ", "-EQ ", qtPCRAA, indice);
                        ajusta();
                        pos1 = 0;
                        jFrame1.setVisible(false);
                    }
                }
                organiza();
                if (opcao != 0 || !regraCorreta) {
                    testaRegra();
                }
                confirma();
                opcao = 0;
                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração
            }
        }
    }

    @Action
    public void Regra_SP() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 6) {
            //Altera cor do botão
            btnSP.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            lastbtn = 6;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0) {
                if (Teorema[pos1].getFormula().getType() == CONJUNCTION) {
                    regraCorreta = true;
                    //Valida para aplicar a Regra Introdução da equivalência
                    Formula opcao1 = Teorema[pos1].getFormula().getLeft();
                    Formula opcao2 = Teorema[pos1].getFormula().getRight();
                    if (opcao == 0) {
                        popup1(opcao1.display(), opcao2.display());
                    } else if (opcao == 1) {
                        Teorema[++indice] = new Linha(opcao1, " ", "SP ", qtPCRAA, indice);
                        jFrame1.setVisible(false);
                        ajusta();
                        pos1 = 0;
                    } else if (opcao == 2) {
                        Teorema[++indice] = new Linha(opcao2, " ", "SP ", qtPCRAA, indice);
                        jFrame1.setVisible(false);
                        ajusta();
                        pos1 = 0;
                    } else if (opcao == 3) {
                        Teorema[++indice] = new Linha(opcao1, " ", "SP ", qtPCRAA, indice);
                        ajusta();
                        confirma();
                        Teorema[++indice] = new Linha(opcao2, " ", "SP ", qtPCRAA, indice);
                        ajusta();
                        pos1 = 0;
                        jFrame1.setVisible(false);
                    }
                    //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração
                }
                organiza();
                if (opcao != 0 || !regraCorreta) {
                    testaRegra();
                }
                confirma();
                opcao = 0;
            }
        }
    }

    @Action
    public void Regra_EDJ() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 7) {
            //Altera cor do botão
            btnEDJ.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            pos3 = 0;
            lastbtn = 7;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0 && pos2 != 0 && pos3 != 0) {
                //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<<)
                Teorema[pos1].unselect();
                Teorema[pos2].unselect();
                Formula temp1 = null, temp2 = null, temp3 = null;

                if (Teorema[pos1].getFormula().getType() == CONDITIONAL) {
                    temp1 = Teorema[pos1].getFormula();
                    if (Teorema[pos2].getFormula().getType() == CONDITIONAL) {
                        temp2 = Teorema[pos2].getFormula();
                        if (Teorema[pos3].getFormula().getType() == DISJUNCTION) {
                            temp3 = Teorema[pos3].getFormula();
                        }
                    } else if (Teorema[pos3].getFormula().getType() == CONDITIONAL) {
                        temp2 = Teorema[pos3].getFormula();
                        if (Teorema[pos2].getFormula().getType() == DISJUNCTION) {
                            temp3 = Teorema[pos2].getFormula();
                        }
                    }
                } else if (Teorema[pos1].getFormula().getType() == DISJUNCTION) {
                    temp3 = Teorema[pos1].getFormula();
                    if (Teorema[pos2].getFormula().getType() == CONDITIONAL) {
                        temp1 = Teorema[pos2].getFormula();
                        if (Teorema[pos3].getFormula().getType() == CONDITIONAL) {
                            temp2 = Teorema[pos3].getFormula();
                        }
                    }
                }
                if (temp1 != null && temp2 != null && temp3 != null) {
                    //Valida para aplicar a Regra eliminação da disjunção

                    if (temp1.getRight().equalsTo(temp2.getRight())) {
                        if (temp3.getLeft().equalsTo(temp1.getLeft()) && temp3.getRight().equalsTo(temp2.getLeft())
                                || temp3.getRight().equalsTo(temp1.getLeft()) && temp3.getLeft().equalsTo(temp2.getLeft())) {
                            Teorema[++indice] = new Linha(temp1.getRight(), " ", "-DJ ", qtPCRAA, indice);
                            ajusta();
                        }
                    }
                }

                //Atualiza variaveis de controle
                carregar = false;
                pos1 = 0;
                pos2 = 0;
                pos3 = 0;
                organiza();
                testaRegra();
                confirma();
            }
        }
    }

    @Action
    public void Regra_PC() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 8) {
            //Altera cor do botão
            btnPC.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            lastbtn = 8;
            jTextField2.setText(null);
            popup3();
        } else {
            try {
                //Atualiza variaveis de controle
                carregar = false;
                Formula f = new Formula();
                f.parse(jTextField2.getText());
                f = this.eliminaParenteses(f, true);
                if (f.getType() == CONDITIONAL) {
                    ++qtPCRAA;
                    Teorema[++indice] = new Linha(f.getLeft(),
                            f.getRight().display(),
                            "HIP-PC ", qtPCRAA, indice);

                    resPCRAA[qtPCRAA - 1] = f.display();
                    resPCRAA[50 - qtPCRAA] = "pc";

                    Teorema[indice].setFormula(eliminaParenteses(Teorema[indice].getFormula(), true));
                    organiza();
                    alteraCor();
                    btnDesfazer.setEnabled(true);
                    comunicaServidor("diag_prova", "regra aplicada");
                    confirma();
                } else {
                    JOptionPane.showMessageDialog(null, "Fórmula sem implicação.");
                }
            } catch (ScannerException ex) {
                JOptionPane.showMessageDialog(null, "Erro na fórmula.");
            } catch (ParserException ex) {
                JOptionPane.showMessageDialog(null, "Erro na fórmula.");
            }
        }

    }

    @Action
    public void Regra_RAA() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 9) {
            //Altera cor do botão
            btnRAA.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            //Atualiza variaveis de controle
            lastbtn = 9;
            jTextField2.setText(null);
            popup3();
        } else {
            try {
                //Atualiza variaveis de controle
                carregar = false;
                Formula f = new Formula();
                f.parse(jTextField2.getText());
                f = this.eliminaParenteses(f, true);
                ++qtPCRAA;
                Teorema[++indice] = new Linha(f, " ", "HIP-RAA ", qtPCRAA, indice);
                resPCRAA[qtPCRAA - 1] = jTextField2.getText();
                resPCRAA[50 - qtPCRAA] = "raa";

                ajusta();
                regraCorreta = false;

                organiza();
                btnDesfazer.setEnabled(true);

                comunicaServidor("diag_prova", "regra aplicada");
                alteraCor();
                confirma();
            } catch (ScannerException ex) {
                JOptionPane.showMessageDialog(null, "Erro na fórmula.");
            } catch (ParserException ex) {
                JOptionPane.showMessageDialog(null, "Erro na fórmula.");
            }
        }
    }

    @Action
    public void Regra_DN() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 10) {
            //Altera cor do botão
            btnDN.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            lastbtn = 10;
        } else {
            if (pos1 != 0) {
                Formula f = Teorema[pos1].getFormula();
                if (f.getType() == NEGATION) {
                    if (f.getNext().getType() == NEGATION) {
                        Teorema[++indice] = new Linha(f.getNext().getNext(), " ", "DN ", qtPCRAA, indice);
                        ajusta();
                    }
                }

                //Atualiza variaveis de controle
                pos1 = 0;
                organiza();
                testaRegra();
                confirma();
            }
            carregar = false;
        }
    }

    @Action
    public void Regra_MT() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 11) {
            //Altera cor do botão
            btnMT.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 11;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0 && pos2 != 0) {
                //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<<)
                Teorema[pos1].unselect();

                //Valida para aplicar a Regra Modus Tollens
                if (Teorema[pos1].getFormula().display().length() < Teorema[pos2].getFormula().display().length() && Teorema[pos2].getFormula().getType() == CONDITIONAL) {
                    if (Teorema[pos2].getFormula().getRight().getType() == NEGATION) {
                        if (Teorema[pos2].getFormula().getRight().getNext().equalsTo(Teorema[pos1].getFormula()))//analisa se a regra modus pones pode ser aplicada
                        {
                            Teorema[++indice] = new Linha(new Formula(NEGATION, Teorema[pos2].getFormula().getLeft()), " ", "MT ", qtPCRAA, indice);
                            ajusta();
                        }
                    } else if (Teorema[pos1].getFormula().getType() == NEGATION) {
                        if (Teorema[pos2].getFormula().getRight().equalsTo(Teorema[pos1].getFormula().getNext()))//analisa se a regra modus pones pode ser aplicada
                        {
                            Teorema[++indice] = new Linha(new Formula(NEGATION, Teorema[pos2].getFormula().getLeft()), " ", "MT ", qtPCRAA, indice);
                            ajusta();
                        }
                    }
                } else if (Teorema[pos1].getFormula().display().length() > Teorema[pos2].getFormula().display().length() && Teorema[pos1].getFormula().getType() == CONDITIONAL) {
                    if (Teorema[pos1].getFormula().getRight().getType() == NEGATION) {
                        if (Teorema[pos1].getFormula().getRight().getNext().equalsTo(Teorema[pos2].getFormula()))//analisa se a regra modus pones pode ser aplicada
                        {
                            Teorema[++indice] = new Linha(new Formula(NEGATION, Teorema[pos1].getFormula().getLeft()), " ", "MT ", qtPCRAA, indice);
                            ajusta();
                        }
                    } else if (Teorema[pos2].getFormula().getType() == NEGATION) {
                        if (Teorema[pos1].getFormula().getRight().equalsTo(Teorema[pos2].getFormula().getNext()))//analisa se a regra modus pones pode ser aplicada
                        {
                            Teorema[++indice] = new Linha(new Formula(NEGATION, Teorema[pos1].getFormula().getLeft()), " ", "MT ", qtPCRAA, indice);
                            ajusta();
                        }
                    }
                }

                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração
                pos1 = 0;
                pos2 = 0;

                //Atualiza variaveis de controle
                carregar = false;
                organiza();
                testaRegra();
                confirma();
            }
        }
    }

    @Action
    public void Regra_SH() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 12) {
            //Altera cor do botão
            btnSH.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 12;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0 && pos2 != 0) {
                //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<<)
                Teorema[pos1].unselect();

                //Valida para aplicar a Regra Silogismo Hipotético
                if (Teorema[pos1].getFormula().getType() == CONDITIONAL && Teorema[pos2].getFormula().getType() == CONDITIONAL) {
                    if (Teorema[pos1].getFormula().getRight().equalsTo(Teorema[pos2].getFormula().getLeft())) {
                        Teorema[++indice] = new Linha(new Formula(CONDITIONAL, Teorema[pos1].getFormula().getLeft(), Teorema[pos2].getFormula().getRight()),
                                " ", "SH ", qtPCRAA, indice);
                        ajusta();
                    } else if (Teorema[pos2].getFormula().getRight().equalsTo(Teorema[pos1].getFormula().getLeft())) {
                        Teorema[++indice] = new Linha(new Formula(CONDITIONAL, Teorema[pos2].getFormula().getLeft(), Teorema[pos1].getFormula().getRight()),
                                " ", "SH ", qtPCRAA, indice);
                        ajusta();
                    }
                }

                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração
                pos1 = 0;
                pos2 = 0;

                //Atualiza variaveis de controle
                carregar = false;
                organiza();
                testaRegra();
                confirma();
            }
        }
    }

    @Action
    public void Regra_SD() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 13) {
            //Altera cor do botão
            btnSD.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 13;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0 && pos2 != 0) {
                //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<<)
                Teorema[pos1].unselect();

                Formula f;
                //Valida para aplicar a Regra Silogismo Hipotético
                if (Teorema[pos1].getFormula().getType() == DISJUNCTION) {
                    if (Teorema[pos2].getFormula().getType() == NEGATION) {
                        f = Teorema[pos2].getFormula().getNext();
                    } else {
                        f = new Formula(NEGATION, Teorema[pos2].getFormula());
                    }
                    if (f.equalsTo(Teorema[pos1].getFormula().getRight())) {
                        Teorema[++indice] = new Linha(Teorema[pos1].getFormula().getLeft(), " ", "SD ", qtPCRAA, indice);
                        ajusta();
                    }
                    if (f.equalsTo(Teorema[pos1].getFormula().getLeft())) {
                        Teorema[++indice] = new Linha(Teorema[pos1].getFormula().getRight(), " ", "SD ", qtPCRAA, indice);
                        ajusta();
                    }
                } else if (Teorema[pos2].getFormula().getType() == DISJUNCTION) {
                    if (Teorema[pos1].getFormula().getType() == NEGATION) {
                        f = Teorema[pos1].getFormula().getNext();
                    } else {
                        f = new Formula(NEGATION, Teorema[pos1].getFormula());
                    }
                    if (f.equalsTo(Teorema[pos2].getFormula().getRight())) {
                        Teorema[++indice] = new Linha(Teorema[pos2].getFormula().getLeft(), " ", "SD ", qtPCRAA, indice);
                        ajusta();
                    }
                    if (f.equalsTo(Teorema[pos2].getFormula().getLeft())) {
                        Teorema[++indice] = new Linha(Teorema[pos2].getFormula().getRight(), " ", "SD ", qtPCRAA, indice);
                        ajusta();
                    }
                }
                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração
                pos1 = 0;
                pos2 = 0;

                //Atualiza variaveis de controle
                carregar = false;
                organiza();
                testaRegra();
                confirma();
            }
        }
    }

    @Action
    public void Regra_INC() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 14) {
            //Altera cor do botão
            btnINC.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 14;
            jTextField2.setText(null);
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0 && pos2 != 0) {
                //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<<)
                Teorema[pos1].unselect();

                //Valida para aplicar a Regra Inconsistência
                if (Teorema[pos1].getFormula().getType() == NEGATION) {
                    if (Teorema[pos1].getFormula().getNext().equalsTo(Teorema[pos2].getFormula())) {
                        popup3();
                        regraCorreta = true;
                    }
                } else if (Teorema[pos2].getFormula().getType() == NEGATION) {
                    if (Teorema[pos2].getFormula().getNext().equalsTo(Teorema[pos1].getFormula())) {
                        popup3();
                        regraCorreta = true;
                    }
                }
                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração

                //Atualiza variaveis de controle
                carregar = false;
                organiza();
                testaRegra();
                confirma();
            }
        }
    }

    private void aplicaINC() {
        try {
            Formula f = new Formula();
            f.parse(jTextField2.getText());
            f = this.eliminaParenteses(f, true);
            Teorema[++indice] = new Linha(f, " ", "INC ", qtPCRAA, indice);

            ajusta();
            regraCorreta = false;

            organiza();

            comunicaServidor("diag_prova", "regra aplicada");
            alteraCor();
            confirma();
        } catch (ScannerException ex) {
            JOptionPane.showMessageDialog(null, "Erro na fórmula");
        } catch (ParserException ex) {
            JOptionPane.showMessageDialog(null, "Erro na fórmula");
        }
        pos1 = 0;
        pos2 = 0;
    }

    @Action
    public void Regra_DC() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 15) {
            //Altera cor do botão
            btnDC.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            pos3 = 0;
            lastbtn = 15;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0 && pos2 != 0 && pos3 != 0) {
                //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<<)
                Teorema[pos1].unselect();
                Teorema[pos2].unselect();
                Formula temp1 = null, temp2 = null, temp3 = null;

                if (Teorema[pos1].getFormula().getType() == CONDITIONAL) {
                    temp1 = Teorema[pos1].getFormula();
                    if (Teorema[pos2].getFormula().getType() == CONDITIONAL) {
                        temp2 = Teorema[pos2].getFormula();
                        if (Teorema[pos3].getFormula().getType() == DISJUNCTION) {
                            temp3 = Teorema[pos3].getFormula();
                        }
                    } else if (Teorema[pos3].getFormula().getType() == CONDITIONAL) {
                        temp2 = Teorema[pos3].getFormula();
                        if (Teorema[pos2].getFormula().getType() == DISJUNCTION) {
                            temp3 = Teorema[pos2].getFormula();
                        }
                    }
                } else if (Teorema[pos1].getFormula().getType() == DISJUNCTION) {
                    temp3 = Teorema[pos1].getFormula();
                    if (Teorema[pos2].getFormula().getType() == CONDITIONAL) {
                        temp1 = Teorema[pos2].getFormula();
                        if (Teorema[pos3].getFormula().getType() == CONDITIONAL) {
                            temp2 = Teorema[pos3].getFormula();
                        }
                    }
                }
                if (temp1 != null && temp2 != null && temp3 != null) {
                    //Valida para aplicar a Regra eliminação da disjunção

                    if (temp3.getRight().equalsTo(temp2.getLeft())) {
                        if (temp3.getLeft().equalsTo(temp1.getLeft())) {
                            Formula f = new Formula(DISJUNCTION, temp1.getRight(), temp2.getRight());
                            Teorema[++indice] = new Linha(f, " ", "DC ", qtPCRAA, indice);
                            ajusta();
                        }
                    } else {
                        if (temp3.getRight().equalsTo(temp1.getLeft())) {
                            if (temp3.getLeft().equalsTo(temp2.getLeft())) {
                                Formula f = new Formula(DISJUNCTION, temp1.getRight(), temp2.getRight());
                                Teorema[++indice] = new Linha(f, " ", "DC ", qtPCRAA, indice);
                                ajusta();
                            }
                        }
                    }
                }
                //Atualiza variaveis de controle
                carregar = false;
                pos1 = 0;
                pos2 = 0;
                pos3 = 0;
                organiza();
                testaRegra();
                confirma();
            }
        }
    }

    @Action
    public void Regra_EXP() {
        alteraCor();
        //Executa a ação do usuário
        if (!carregar || lastbtn != 16) {
            //Altera cor do botão
            btnEXP.setBackground(Color.RED);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            lastbtn = 16;
        } else {
            //Atualiza variaveis de controle
            carregar = false;
            if (pos1 != 0) {
                if (Teorema[pos1].getFormula().getType() == CONDITIONAL) {
                    Formula f = Teorema[pos1].getFormula().getLeft();
                    while (f.getType() == PARENTHESIS) {
                        f = f.getNext();
                    }
                    if (f.getType() == CONJUNCTION) {
                        Formula aux = new Formula(CONDITIONAL, f.getRight(), Teorema[pos1].getFormula().getRight());
                        aux = new Formula(PARENTHESIS, aux);
                        aux = new Formula(CONDITIONAL, f.getLeft(), aux);
                        Teorema[++indice] = new Linha(aux, " ", "EXP ", qtPCRAA, indice);
                        ajusta();
                    }
                }
                //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração
                pos1 = 0;

                //Atualiza variaveis de controle
                carregar = false;
                organiza();
                testaRegra();
                confirma();
            }
        }
    }

    @Action
    public void Limpar() {

        //Zera todas as variaveis de controle dos teoremas
        Teorema = new Linha[100];
        TeoremaAux = Teorema.clone();
        qtPCRAA = 0;
        //btnIniciar.setEnabled(false);
        jComboBox1.setEnabled(false);
        //Limpa as variaveis de tela
        lstTeorema.clearSelection();
        lstTeorema.setListData(Teorema);
        //txtTeorema.setEditable(true);
        this.setBotoes(false, false, false);
        btnRefazer.setEnabled(false);
        btnDesfazer.setEnabled(false);

        txtArgumento.setVisible(false);//COrrigir para próxima versão
        jComboBox1.setVisible(false);
        btnIniciar.setVisible(false);
        //Atualiza as variaveis de controle e cores dos botões
        pos1 = 0;
        pos2 = 0;
        pos3 = 0;
        indice = 0;
        indiceoriginal = 0;
        carregar = false;
        alteraCor();
        msgAgent.clear();
        lstMensagem.setListData(msgAgent.toArray());
        qtAjuda = 0;
        if (jSplitPane1.getRightComponent() != null) {
            jSplitPane1.remove(2);
        }
    }

    private void setBotoes(boolean set, boolean set2, boolean set3) {
        //set valida os botões das regras, set2 os botões das hipoteses e set3 os demais botões
        jButton11.setEnabled(set2);
        jButton13.setEnabled(set2);
        btnMaiorLetra.setEnabled(set3);
        btnMenorLetra.setEnabled(set3);
        btnLimpar.setEnabled(set3);
        btnMP.setEnabled(set);
        btnAD.setEnabled(set);
        btnCJ.setEnabled(set);
        btnEEQ.setEnabled(set);
        btnIEQ.setEnabled(set);
        btnDN.setEnabled(set);
        btnPC.setEnabled(set);
        btnRAA.setEnabled(set);
        btnSP.setEnabled(set);
        btnEDJ.setEnabled(set);
        btnMT.setEnabled(set);
        btnINC.setEnabled(set);
        btnEXP.setEnabled(set);
        btnSD.setEnabled(set);
        btnSH.setEnabled(set);
        btnDC.setEnabled(set);
    }

    private void confirma() {
        if (qtPCRAA > 0) {
            if (resPCRAA[50 - qtPCRAA].equals("pc")) {
                confirmaPC();
            } else {
                confirmaRAA();
            }
        } else //testa se a prova está completa
        if (Teorema[indice].getFormula().equalsTo(Teorema[0].getFormula())) {
            lstTeorema.setEnabled(false);
            this.setBotoes(false, false, true);
            btnDesfazer.setEnabled(false);
            btnRefazer.setEnabled(false);
            if (this.resolucao == null) {
                JOptionPane.showMessageDialog(null, "Argumento provado com sucesso.");
            } else {
                if (JOptionPane.showConfirmDialog(null, "Argumento provado com sucesso. Deseja ver a resolução do provador?", "", JOptionPane.YES_NO_OPTION) == JOptionPane.YES_OPTION) {
                    jSplitPane1.add(jScrollPane3);
                    jSplitPane1.setDividerLocation(jSplitPane1.getWidth() / 2);
                    lstProvador.setListData(this.resolucao);
                }
            }
        }
    }

    private void confirmaPC() {
        try {
            //testa se a regra PC pode ser finalizada
            Formula f = new Formula();
            f.parse(resPCRAA[qtPCRAA - 1]);
            if (Teorema[indice].getFormula().equalsTo(f.getRight())) {
                --qtPCRAA;
                Teorema[++indice] = new Linha(resPCRAA[qtPCRAA], " ", "PC ", qtPCRAA, indice);
                terminaPCRAA();

                ajustaPCRAA();
                confirma();
                organiza();
                comunicaServidor("diag_prova", "regra aplicada");
            }
        } catch (ScannerException ex) {
            Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE, null, ex);
        } catch (ParserException ex) {
            Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE, null, ex);
        }
    }

    private void confirmaRAA() {//testa se há um absurdo
        Formula temp = Teorema[indice].getFormula();
        if (temp.getType() == CONJUNCTION) {
            try {
                Formula f = new Formula();
                f.parse(resPCRAA[qtPCRAA - 1]);
                if (temp.getLeft().getType() == NEGATION) {
                    if (temp.getLeft().getNext().equalsTo(temp.getRight())) {
                        --qtPCRAA;
                        if (f.getType() != PROPOSITION && f.getType() != PARENTHESIS && f.getType() != NEGATION) {
                            Teorema[++indice] = new Linha("~(" + resPCRAA[qtPCRAA] + ")", " ", "RAA ", qtPCRAA, indice);
                        } else {
                            Teorema[++indice] = new Linha("~" + resPCRAA[qtPCRAA], " ", "RAA ", qtPCRAA, indice);
                        }
                        terminaPCRAA();
                        organiza();
                        confirma();
                        ajustaPCRAA();
                        comunicaServidor("diag_prova", "regra aplicada");
                    }
                } else if (temp.getRight().getType() == NEGATION) {
                    if (temp.getRight().getNext().equalsTo(temp.getLeft())) {
                        --qtPCRAA;
                        if (f.getType() != PROPOSITION && f.getType() != PARENTHESIS && f.getType() != NEGATION) {
                            Teorema[++indice] = new Linha("~(" + resPCRAA[qtPCRAA] + ")", " ", "RAA ", qtPCRAA, indice);
                        } else {
                            Teorema[++indice] = new Linha("~" + resPCRAA[qtPCRAA], " ", "RAA ", qtPCRAA, indice);
                        }
                        terminaPCRAA();
                        organiza();
                        confirma();
                        ajustaPCRAA();
                        comunicaServidor("diag_prova", "regra aplicada");
                    }
                }
            } catch (ScannerException ex) {
                Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE, null, ex);
            } catch (ParserException ex) {
                Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE, null, ex);
            }
        }
    }

    private void ajusta() {//ajusta Teorema[indice] com os nº das linhas e com a regra utilizada
        regraCorreta = true;
        Teorema[indice].setFormula(eliminaParenteses(Teorema[indice].getFormula(), true));
        if (Teorema[indice].getPos().equals(" ")) {
            if (pos1 == 0) {
                Teorema[indice].setPos("");
            } else if (pos2 == 0) {
                Teorema[indice].setPos("" + pos1);
            } else if (pos3 == 0) {
                if (pos1 < pos2) {
                    Teorema[indice].setPos(pos1 + "," + pos2);
                } else {
                    Teorema[indice].setPos(pos2 + "," + pos1);
                }
            } else if (pos1 < pos2) {
                if (pos1 < pos3) {
                    if (pos2 < pos3) {
                        Teorema[indice].setPos(pos1 + "," + pos2 + "," + pos3);
                    } else {
                        Teorema[indice].setPos(pos1 + "," + pos3 + "," + pos2);
                    }
                } else {
                    Teorema[indice].setPos(pos3 + "," + pos1 + "," + pos2);
                }
            } else if (pos2 < pos3) {
                if (pos1 < pos3) {
                    Teorema[indice].setPos(pos2 + "," + pos1 + "," + pos3);
                } else {
                    Teorema[indice].setPos(pos2 + "," + pos3 + "," + pos1);
                }
            } else {
                Teorema[indice].setPos(pos3 + "," + pos2 + "," + pos1);
            }
        }
    }

    private void ajustaPCRAA() {
        for (int x = indice - 1; x > 0; --x) {
            if (Teorema[x].isUsable()) {
                Teorema[indice].setPos((x + 1) + "-" + (indice - 1));
                return;
            }
        }
        Teorema[indice].setPos("1-" + (indice - 1));
    }

    private void organiza() {
        indiceoriginal = indice;

        lstTeorema.clearSelection(); //Limpa lista
        lstTeorema.setListData(Teorema); //Carrega lista com os novos dados do Teorema

        TeoremaAux = Teorema.clone(); //Atualiza a lista auxiliar do teorema
    }

    @Action
    public void Salvar() {
        jFileChooser1.setAcceptAllFileFilterUsed(false);
        int returnVal = jFileChooser1.showSaveDialog(jFileChooser1.getParent());//Abre a janela para salvar o arquivo
        if (returnVal == JFileChooser.APPROVE_OPTION) {//confere se o usuario não cancelou a operação
            File f = jFileChooser1.getSelectedFile();//atribui a f o arquivo selecionado
            if (f != null)//confere se o arquivo selecionado não é null
            {
                try {
                    f = ajustaFile(f);
                    FileOutputStream fos = new FileOutputStream(f);
                    ObjectOutputStream os = new ObjectOutputStream(fos);
                    os.writeObject(qtPCRAA);
                    os.writeObject(resPCRAA);
                    os.writeObject(Teorema);
                    os.close();

                    FileWriter fr = new FileWriter(ajustaFiletxt(f));
                    PrintWriter out = new PrintWriter(fr);
                    //salva as informações no arquivo
                    for (int x = 0; x <= indice; ++x) {
                        out.println(Teorema[x]);
                    }
                    out.close();
                } catch (IOException e) {
                    JOptionPane.showMessageDialog(null, "Erro ao salvar o arquivo");
                }
            }
        }
    }

    @Action
    public void Abrir() {
        jFileChooser1.setAcceptAllFileFilterUsed(false);
        jFileChooser1.setSelectedFile(new File(""));
        int returnVal = jFileChooser1.showOpenDialog(jFileChooser1.getParent());//Abre a janela para abrir o arquivo
        if (returnVal == JFileChooser.APPROVE_OPTION) {//confere se o usuario não cancelou a operação
            lstTeorema.setEnabled(true);
            File f = jFileChooser1.getSelectedFile();//atribui a f o arquivo selecionado
            abre(f);
        }
    }

    public void abre(File f) {
        if (f != null)//confere se o arquivo selecionado não é null
        {
            try {
                FileInputStream fos = new FileInputStream(f);
                ObjectInputStream os = new ObjectInputStream(fos);
                qtPCRAA = (Integer) os.readObject();
                resPCRAA = (String[]) os.readObject();
                Teorema = (Linha[]) os.readObject();
                if (Teorema[0] == null) {
                    Limpar();
                } else {
                    for (indice = 0; Teorema[indice] != null; ++indice);
                    --indice;
                    organiza();
                    if (indice >= 0) {
                        String aux[] = Teorema[0].toString().split(",");
                        aux[0] = aux[0].substring(aux[0].indexOf(":") + 1);
                        if (aux.length > indice) {
                            boolean hipAdicionada = false;
                            int qtHip = 0;
                            total_hipoteses = aux.length;
                            hipoteses = new Formula[total_hipoteses];
                            try {
                                Formula f1;
                                for (int x = 0; x < total_hipoteses; ++x) {
                                    if (!aux[x].contains("|-")) {
                                        f1 = new Formula();
                                        f1.parse(aux[x]);
                                    } else {
                                        f1 = new Formula();
                                        f1.parse(aux[x].substring(0, aux[x].indexOf("|-")));
                                    }
                                    for (int y = 1; y < indice + 1; ++y) {
                                        if (f1.equalsTo(Teorema[y].getFormula())) {
                                            hipAdicionada = true;
                                        }
                                    }
                                    if (!hipAdicionada) {
                                        hipoteses[qtHip++] = f1;
                                    } else {
                                        hipAdicionada = false;
                                    }
                                }
                            } catch (ScannerException e) {
                                Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE, null, e);
                            } catch (ParserException ex) {
                                Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE, null, ex);
                            }
                            setBotoes(false, true, true);
                        } else {
                            setBotoes(true, false, true);
                        }
                        if (indice > 0) {
                            if (Teorema[indice].getFormula().equalsTo(Teorema[0].getFormula())) {
                                lstTeorema.setEnabled(false);
                                this.setBotoes(false, false, true);
                                btnDesfazer.setEnabled(false);
                            }
                        }
                    }
                }
                fos.close();
                os.close();
            } catch (IOException e) {
                JOptionPane.showMessageDialog(null, e);
            } catch (ClassNotFoundException ex) {
                JOptionPane.showMessageDialog(null, ex);
            }
        }

    }

    private File ajustaFile(File f) {//ajusta o aruivo selecionado para que termine com .her
        String aux = f.getAbsolutePath();
        if (aux.length() < 4) {
            aux += ".her";
        } else if (!aux.substring(aux.length() - 4).equals(".her")) {
            aux += ".her";
        }
        return new File(aux);
    }

    private File ajustaFiletxt(File f) {//ajusta o aruivo selecionado para que termine com .txt
        String aux = f.getAbsolutePath();
        aux = aux.substring(0, aux.length() - 4) + ".txt";
        return new File(aux);
    }

    private Formula eliminaParenteses(Formula f, boolean root) {
        if (root) {
            while (f.getType() == PARENTHESIS) {
                f = f.getNext();
            }
        }

        if (f.getType() == NEGATION) {
            f.setNext(eliminaParenteses(f.getNext(), false));
        }
        if (f.getType() == PARENTHESIS) {
            if (f.getNext().getType() == PARENTHESIS) {
                f = f.getNext();
                f = eliminaParenteses(f, false);
            }
            f.setNext(eliminaParenteses(f.getNext(), false));

        }
        if (f.getLeft() != null) {
            if (f.getLeft().getType() == PARENTHESIS
                    && (f.getLeft().getNext().getType() == PROPOSITION
                    || f.getLeft().getNext().getType() == NEGATION
                    || f.getLeft().getNext().getType() == PARENTHESIS)) {
                f.setLeft(f.getLeft().getNext());
                f = eliminaParenteses(f, false);
            }
            f.setLeft(eliminaParenteses(f.getLeft(), false));
        }
        if (f.getRight() != null) {
            if (f.getRight().getType() == PARENTHESIS
                    && (f.getRight().getNext().getType() == PROPOSITION
                    || f.getRight().getNext().getType() == NEGATION
                    || f.getRight().getNext().getType() == PARENTHESIS)) {
                f.setRight(f.getRight().getNext());
                f = eliminaParenteses(f, false);
            }
            f.setRight(eliminaParenteses(f.getRight(), false));
        }
        return f;
    }

    @SuppressWarnings("unchecked")
    // <editor-fold defaultstate="collapsed" desc="Generated Code">//GEN-BEGIN:initComponents
    private void initComponents() {

        jFrame1 = new javax.swing.JFrame();
        jLabel38 = new javax.swing.JLabel();
        btnDireita = new javax.swing.JButton();
        btnEsquerda = new javax.swing.JButton();
        btnAmbos = new javax.swing.JButton();
        jButton6 = new javax.swing.JButton();
        jFrame2 = new javax.swing.JFrame();
        jLabel39 = new javax.swing.JLabel();
        jTextField1 = new javax.swing.JTextField();
        jLabel40 = new javax.swing.JLabel();
        jButton1 = new javax.swing.JButton();
        jButton2 = new javax.swing.JButton();
        jButton7 = new javax.swing.JButton();
        jFrame3 = new javax.swing.JFrame();
        jLabel41 = new javax.swing.JLabel();
        jTextField2 = new javax.swing.JTextField();
        jLabel42 = new javax.swing.JLabel();
        btnOK = new javax.swing.JButton();
        jButton9 = new javax.swing.JButton();
        jFrame5 = new javax.swing.JFrame();
        jFileChooser1 = new javax.swing.JFileChooser();
        jFrame4 = new javax.swing.JFrame();
        jLabel4 = new javax.swing.JLabel();
        ajudaManual = new javax.swing.JRadioButton();
        ajudaExemplos = new javax.swing.JRadioButton();
        ajudaDica = new javax.swing.JRadioButton();
        jButton4 = new javax.swing.JButton();
        buttonGroup1 = new javax.swing.ButtonGroup();
        btnIniciar = new javax.swing.JButton();
        jLabel1 = new javax.swing.JLabel();
        pnlRegras = new javax.swing.JPanel();
        btnSH = new javax.swing.JButton();
        jLabel2 = new javax.swing.JLabel();
        btnRAA = new javax.swing.JButton();
        btnDN = new javax.swing.JButton();
        btnPC = new javax.swing.JButton();
        btnMP = new javax.swing.JButton();
        btnCJ = new javax.swing.JButton();
        btnSP = new javax.swing.JButton();
        btnAD = new javax.swing.JButton();
        btnEDJ = new javax.swing.JButton();
        btnIEQ = new javax.swing.JButton();
        btnEEQ = new javax.swing.JButton();
        jLabel3 = new javax.swing.JLabel();
        btnMT = new javax.swing.JButton();
        btnSD = new javax.swing.JButton();
        btnINC = new javax.swing.JButton();
        btnEXP = new javax.swing.JButton();
        btnDC = new javax.swing.JButton();
        jLabel5 = new javax.swing.JLabel();
        jLabel12 = new javax.swing.JLabel();
        jLabel13 = new javax.swing.JLabel();
        jLabel14 = new javax.swing.JLabel();
        jLabel15 = new javax.swing.JLabel();
        jLabel16 = new javax.swing.JLabel();
        jSeparator3 = new javax.swing.JSeparator();
        btnDesfazer = new javax.swing.JButton();
        btnRefazer = new javax.swing.JButton();
        btnLimpar = new javax.swing.JButton();
        btnMaiorLetra = new javax.swing.JButton();
        btnMenorLetra = new javax.swing.JButton();
        jSeparator2 = new javax.swing.JSeparator();
        jButton11 = new javax.swing.JButton();
        jButton13 = new javax.swing.JButton();
        jButton3 = new javax.swing.JButton();
        labelIsLogado = new javax.swing.JLabel();
        btnLogar = new javax.swing.JButton();
        jLabel6 = new javax.swing.JLabel();
        jLabel17 = new javax.swing.JLabel();
        jLabel18 = new javax.swing.JLabel();
        jLabel19 = new javax.swing.JLabel();
        jLabel20 = new javax.swing.JLabel();
        jLabel21 = new javax.swing.JLabel();
        jLabel7 = new javax.swing.JLabel();
        jLabel22 = new javax.swing.JLabel();
        jSeparator1 = new javax.swing.JSeparator();
        jComboBox1 = new javax.swing.JComboBox();
        jComboBox2 = new javax.swing.JComboBox();
        jScrollPane2 = new javax.swing.JScrollPane();
        lstMensagem = new javax.swing.JList();
        jSplitPane1 = new javax.swing.JSplitPane();
        jScrollPane1 = new javax.swing.JScrollPane();
        lstTeorema = new javax.swing.JList();
        jScrollPane3 = new javax.swing.JScrollPane();
        lstProvador = new javax.swing.JList();
        txtArgumento = new javax.swing.JTextField();
        jLabel8 = new javax.swing.JLabel();

        jFrame1.setName("jFrame1"); // NOI18N

        org.jdesktop.application.ResourceMap resourceMap = org.jdesktop.application.Application.getInstance(heraclito.HeraclitoApp.class).getContext().getResourceMap(Edicao.class);
        jLabel38.setText(resourceMap.getString("jLabel38.text")); // NOI18N
        jLabel38.setName("jLabel38"); // NOI18N

        javax.swing.ActionMap actionMap = org.jdesktop.application.Application.getInstance(heraclito.HeraclitoApp.class).getContext().getActionMap(Edicao.class, this);
        btnDireita.setAction(actionMap.get("btn1")); // NOI18N
        btnDireita.setText(resourceMap.getString("btnDireita.text")); // NOI18N
        btnDireita.setName("btnDireita"); // NOI18N

        btnEsquerda.setAction(actionMap.get("btn2")); // NOI18N
        btnEsquerda.setText(resourceMap.getString("btnEsquerda.text")); // NOI18N
        btnEsquerda.setName("btnEsquerda"); // NOI18N

        btnAmbos.setAction(actionMap.get("btn3")); // NOI18N
        btnAmbos.setText(resourceMap.getString("btnAmbos.text")); // NOI18N
        btnAmbos.setName("btnAmbos"); // NOI18N

        jButton6.setAction(actionMap.get("btnCancela")); // NOI18N
        jButton6.setText(resourceMap.getString("jButton6.text")); // NOI18N
        jButton6.setName("jButton6"); // NOI18N

        javax.swing.GroupLayout jFrame1Layout = new javax.swing.GroupLayout(jFrame1.getContentPane());
        jFrame1.getContentPane().setLayout(jFrame1Layout);
        jFrame1Layout.setHorizontalGroup(
            jFrame1Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame1Layout.createSequentialGroup()
                .addContainerGap()
                .addGroup(jFrame1Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                    .addComponent(jLabel38)
                    .addGroup(jFrame1Layout.createSequentialGroup()
                        .addGroup(jFrame1Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.TRAILING)
                            .addComponent(jButton6)
                            .addGroup(jFrame1Layout.createSequentialGroup()
                                .addComponent(btnDireita)
                                .addGap(18, 18, 18)
                                .addComponent(btnEsquerda)))
                        .addGap(18, 18, 18)
                        .addComponent(btnAmbos)))
                .addContainerGap(javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
        );
        jFrame1Layout.setVerticalGroup(
            jFrame1Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame1Layout.createSequentialGroup()
                .addContainerGap()
                .addComponent(jLabel38, javax.swing.GroupLayout.PREFERRED_SIZE, 32, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addGap(18, 18, 18)
                .addGroup(jFrame1Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(btnDireita)
                    .addComponent(btnEsquerda)
                    .addComponent(btnAmbos))
                .addGap(18, 18, 18)
                .addComponent(jButton6)
                .addContainerGap(javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
        );

        jFrame2.setName("jFrame2"); // NOI18N

        jLabel39.setText(resourceMap.getString("jLabel39.text")); // NOI18N
        jLabel39.setName("jLabel39"); // NOI18N

        jTextField1.setText(resourceMap.getString("jTextField1.text")); // NOI18N
        jTextField1.setName("jTextField1"); // NOI18N

        jLabel40.setText(resourceMap.getString("jLabel40.text")); // NOI18N
        jLabel40.setName("jLabel40"); // NOI18N

        jButton1.setAction(actionMap.get("btn1")); // NOI18N
        jButton1.setName("jButton1"); // NOI18N

        jButton2.setAction(actionMap.get("btn2")); // NOI18N
        jButton2.setName("jButton2"); // NOI18N

        jButton7.setAction(actionMap.get("btnCancela")); // NOI18N
        jButton7.setText(resourceMap.getString("jButton7.text")); // NOI18N
        jButton7.setName("jButton7"); // NOI18N

        javax.swing.GroupLayout jFrame2Layout = new javax.swing.GroupLayout(jFrame2.getContentPane());
        jFrame2.getContentPane().setLayout(jFrame2Layout);
        jFrame2Layout.setHorizontalGroup(
            jFrame2Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame2Layout.createSequentialGroup()
                .addContainerGap()
                .addGroup(jFrame2Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                    .addComponent(jButton1, javax.swing.GroupLayout.DEFAULT_SIZE, 177, Short.MAX_VALUE)
                    .addComponent(jButton2, javax.swing.GroupLayout.DEFAULT_SIZE, 177, Short.MAX_VALUE)
                    .addComponent(jLabel40, javax.swing.GroupLayout.DEFAULT_SIZE, 177, Short.MAX_VALUE)
                    .addComponent(jTextField1, javax.swing.GroupLayout.DEFAULT_SIZE, 177, Short.MAX_VALUE)
                    .addComponent(jLabel39, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                .addContainerGap(18, Short.MAX_VALUE))
            .addGroup(jFrame2Layout.createSequentialGroup()
                .addGap(60, 60, 60)
                .addComponent(jButton7)
                .addContainerGap(70, Short.MAX_VALUE))
        );
        jFrame2Layout.setVerticalGroup(
            jFrame2Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame2Layout.createSequentialGroup()
                .addGap(20, 20, 20)
                .addComponent(jLabel39, javax.swing.GroupLayout.PREFERRED_SIZE, 29, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addGap(18, 18, 18)
                .addComponent(jTextField1, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addGap(46, 46, 46)
                .addComponent(jLabel40, javax.swing.GroupLayout.PREFERRED_SIZE, 28, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addGap(20, 20, 20)
                .addComponent(jButton1, javax.swing.GroupLayout.DEFAULT_SIZE, 23, Short.MAX_VALUE)
                .addGap(18, 18, 18)
                .addComponent(jButton2, javax.swing.GroupLayout.DEFAULT_SIZE, 23, Short.MAX_VALUE)
                .addGap(18, 18, 18)
                .addComponent(jButton7)
                .addContainerGap(61, Short.MAX_VALUE))
        );

        jFrame3.setName("jFrame3"); // NOI18N

        jLabel41.setText(resourceMap.getString("jLabel41.text")); // NOI18N
        jLabel41.setName("jLabel41"); // NOI18N

        jTextField2.setText(resourceMap.getString("jTextField2.text")); // NOI18N
        jTextField2.setName("jTextField2"); // NOI18N

        jLabel42.setText(resourceMap.getString("jLabel42.text")); // NOI18N
        jLabel42.setName("jLabel42"); // NOI18N

        btnOK.setAction(actionMap.get("btnOK")); // NOI18N
        btnOK.setText(resourceMap.getString("btnOK.text")); // NOI18N
        btnOK.setName("btnOK"); // NOI18N

        jButton9.setAction(actionMap.get("btnCancela")); // NOI18N
        jButton9.setText(resourceMap.getString("jButton9.text")); // NOI18N
        jButton9.setName("jButton9"); // NOI18N

        javax.swing.GroupLayout jFrame3Layout = new javax.swing.GroupLayout(jFrame3.getContentPane());
        jFrame3.getContentPane().setLayout(jFrame3Layout);
        jFrame3Layout.setHorizontalGroup(
            jFrame3Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame3Layout.createSequentialGroup()
                .addGroup(jFrame3Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                    .addGroup(jFrame3Layout.createSequentialGroup()
                        .addGap(10, 10, 10)
                        .addComponent(jLabel41, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                    .addGroup(jFrame3Layout.createSequentialGroup()
                        .addContainerGap()
                        .addComponent(jLabel42))
                    .addGroup(jFrame3Layout.createSequentialGroup()
                        .addContainerGap()
                        .addComponent(jTextField2, javax.swing.GroupLayout.PREFERRED_SIZE, 274, javax.swing.GroupLayout.PREFERRED_SIZE))
                    .addGroup(jFrame3Layout.createSequentialGroup()
                        .addGap(58, 58, 58)
                        .addComponent(btnOK)
                        .addGap(58, 58, 58)
                        .addComponent(jButton9)))
                .addContainerGap())
        );
        jFrame3Layout.setVerticalGroup(
            jFrame3Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame3Layout.createSequentialGroup()
                .addContainerGap()
                .addComponent(jLabel41)
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addComponent(jLabel42)
                .addGap(18, 18, 18)
                .addComponent(jTextField2, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addGap(18, 18, 18)
                .addGroup(jFrame3Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(btnOK)
                    .addComponent(jButton9))
                .addContainerGap(23, Short.MAX_VALUE))
        );

        jFrame5.setName("jFrame5"); // NOI18N

        jFileChooser1.setCurrentDirectory(new java.io.File("C:\\Heráclito"));
        jFileChooser1.setDialogType(javax.swing.JFileChooser.SAVE_DIALOG);
        jFileChooser1.setFileFilter(new FileNameExtensionFilter("Heraclito File (*her)","her"));
        jFileChooser1.setCursor(new java.awt.Cursor(java.awt.Cursor.DEFAULT_CURSOR));
        jFileChooser1.setName("jFileChooser1"); // NOI18N

        javax.swing.GroupLayout jFrame5Layout = new javax.swing.GroupLayout(jFrame5.getContentPane());
        jFrame5.getContentPane().setLayout(jFrame5Layout);
        jFrame5Layout.setHorizontalGroup(
            jFrame5Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame5Layout.createSequentialGroup()
                .addContainerGap()
                .addComponent(jFileChooser1, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addContainerGap(javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
        );
        jFrame5Layout.setVerticalGroup(
            jFrame5Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame5Layout.createSequentialGroup()
                .addContainerGap()
                .addComponent(jFileChooser1, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addContainerGap(javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
        );

        jFrame4.setName("jFrame4"); // NOI18N

        jLabel4.setText(resourceMap.getString("jLabel4.text")); // NOI18N
        jLabel4.setName("jLabel4"); // NOI18N

        buttonGroup1.add(ajudaManual);
        ajudaManual.setText(resourceMap.getString("ajudaManual.text")); // NOI18N
        ajudaManual.setName("ajudaManual"); // NOI18N

        buttonGroup1.add(ajudaExemplos);
        ajudaExemplos.setText(resourceMap.getString("ajudaExemplos.text")); // NOI18N
        ajudaExemplos.setName("ajudaExemplos"); // NOI18N

        buttonGroup1.add(ajudaDica);
        ajudaDica.setText(resourceMap.getString("ajudaDica.text")); // NOI18N
        ajudaDica.setName("ajudaDica"); // NOI18N

        jButton4.setAction(actionMap.get("okAjuda")); // NOI18N
        jButton4.setText(resourceMap.getString("jButton4.text")); // NOI18N
        jButton4.setName("jButton4"); // NOI18N

        javax.swing.GroupLayout jFrame4Layout = new javax.swing.GroupLayout(jFrame4.getContentPane());
        jFrame4.getContentPane().setLayout(jFrame4Layout);
        jFrame4Layout.setHorizontalGroup(
            jFrame4Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame4Layout.createSequentialGroup()
                .addContainerGap()
                .addGroup(jFrame4Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                    .addComponent(ajudaDica)
                    .addComponent(ajudaExemplos)
                    .addComponent(ajudaManual)
                    .addComponent(jLabel4)
                    .addComponent(jButton4))
                .addContainerGap(javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
        );
        jFrame4Layout.setVerticalGroup(
            jFrame4Layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(jFrame4Layout.createSequentialGroup()
                .addContainerGap()
                .addComponent(jLabel4)
                .addGap(18, 18, 18)
                .addComponent(ajudaManual)
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.UNRELATED)
                .addComponent(ajudaExemplos)
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.UNRELATED)
                .addComponent(ajudaDica)
                .addGap(18, 18, 18)
                .addComponent(jButton4)
                .addContainerGap(javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
        );

        setBackground(resourceMap.getColor("Form.background")); // NOI18N
        setName("Form"); // NOI18N

        btnIniciar.setAction(actionMap.get("Iniciar")); // NOI18N
        btnIniciar.setText(resourceMap.getString("btnIniciar.text")); // NOI18N
        btnIniciar.setName("btnIniciar"); // NOI18N

        jLabel1.setFont(resourceMap.getFont("jLabel1.font")); // NOI18N
        jLabel1.setText(resourceMap.getString("jLabel1.text")); // NOI18N
        jLabel1.setName("jLabel1"); // NOI18N
        jLabel1.setPreferredSize(new java.awt.Dimension(100, 17));

        pnlRegras.setBackground(resourceMap.getColor("pnlRegras.background")); // NOI18N
        pnlRegras.setBorder(javax.swing.BorderFactory.createLineBorder(new java.awt.Color(0, 0, 0)));
        pnlRegras.setName("pnlRegras"); // NOI18N

        btnSH.setAction(actionMap.get("Regra_SH")); // NOI18N
        btnSH.setText(resourceMap.getString("btnSH.text")); // NOI18N
        btnSH.setToolTipText(resourceMap.getString("btnSH.toolTipText")); // NOI18N
        btnSH.setName("btnSH"); // NOI18N

        jLabel2.setFont(resourceMap.getFont("jLabel2.font")); // NOI18N
        jLabel2.setText(resourceMap.getString("jLabel2.text")); // NOI18N
        jLabel2.setName("jLabel2"); // NOI18N

        btnRAA.setAction(actionMap.get("Regra_RAA")); // NOI18N
        btnRAA.setText(resourceMap.getString("btnRAA.text")); // NOI18N
        btnRAA.setToolTipText(resourceMap.getString("btnRAA.toolTipText")); // NOI18N
        btnRAA.setName("btnRAA"); // NOI18N

        btnDN.setAction(actionMap.get("Regra_DN")); // NOI18N
        btnDN.setText(resourceMap.getString("btnDN.text")); // NOI18N
        btnDN.setToolTipText(resourceMap.getString("btnDN.toolTipText")); // NOI18N
        btnDN.setName("btnDN"); // NOI18N

        btnPC.setAction(actionMap.get("Regra_PC")); // NOI18N
        btnPC.setText(resourceMap.getString("btnPC.text")); // NOI18N
        btnPC.setToolTipText(resourceMap.getString("btnPC.toolTipText")); // NOI18N
        btnPC.setName("btnPC"); // NOI18N

        btnMP.setAction(actionMap.get("Regra_MP")); // NOI18N
        btnMP.setBackground(resourceMap.getColor("btnMP.background")); // NOI18N
        btnMP.setText(resourceMap.getString("btnMP.text")); // NOI18N
        btnMP.setToolTipText(resourceMap.getString("btnMP.toolTipText")); // NOI18N
        btnMP.setName("btnMP"); // NOI18N

        btnCJ.setAction(actionMap.get("Regra_CJ")); // NOI18N
        btnCJ.setText(resourceMap.getString("btnCJ.text")); // NOI18N
        btnCJ.setToolTipText(resourceMap.getString("btnCJ.toolTipText")); // NOI18N
        btnCJ.setName("btnCJ"); // NOI18N

        btnSP.setAction(actionMap.get("Regra_SP")); // NOI18N
        btnSP.setText(resourceMap.getString("btnSP.text")); // NOI18N
        btnSP.setToolTipText(resourceMap.getString("btnSP.toolTipText")); // NOI18N
        btnSP.setName("btnSP"); // NOI18N

        btnAD.setAction(actionMap.get("Regra_AD")); // NOI18N
        btnAD.setFont(resourceMap.getFont("btnAD.font")); // NOI18N
        btnAD.setText(resourceMap.getString("btnAD.text")); // NOI18N
        btnAD.setToolTipText(resourceMap.getString("btnAD.toolTipText")); // NOI18N
        btnAD.setName("btnAD"); // NOI18N

        btnEDJ.setAction(actionMap.get("Regra_EDJ")); // NOI18N
        btnEDJ.setText(resourceMap.getString("btnEDJ.text")); // NOI18N
        btnEDJ.setToolTipText(resourceMap.getString("btnEDJ.toolTipText")); // NOI18N
        btnEDJ.setName("btnEDJ"); // NOI18N

        btnIEQ.setAction(actionMap.get("Regra_IEQ")); // NOI18N
        btnIEQ.setText(resourceMap.getString("btnIEQ.text")); // NOI18N
        btnIEQ.setToolTipText(resourceMap.getString("btnIEQ.toolTipText")); // NOI18N
        btnIEQ.setName("btnIEQ"); // NOI18N

        btnEEQ.setAction(actionMap.get("Regra_EEQ")); // NOI18N
        btnEEQ.setText(resourceMap.getString("btnEEQ.text")); // NOI18N
        btnEEQ.setToolTipText(resourceMap.getString("btnEEQ.toolTipText")); // NOI18N
        btnEEQ.setName("btnEEQ"); // NOI18N

        jLabel3.setBackground(resourceMap.getColor("jLabel3.background")); // NOI18N
        jLabel3.setFont(resourceMap.getFont("jLabel2.font")); // NOI18N
        jLabel3.setText(resourceMap.getString("jLabel3.text")); // NOI18N
        jLabel3.setName("jLabel3"); // NOI18N

        btnMT.setAction(actionMap.get("Regra_MT")); // NOI18N
        btnMT.setText(resourceMap.getString("btnMT.text")); // NOI18N
        btnMT.setToolTipText(resourceMap.getString("btnMT.toolTipText")); // NOI18N
        btnMT.setName("btnMT"); // NOI18N

        btnSD.setAction(actionMap.get("Regra_SD")); // NOI18N
        btnSD.setText(resourceMap.getString("btnSD.text")); // NOI18N
        btnSD.setToolTipText(resourceMap.getString("btnSD.toolTipText")); // NOI18N
        btnSD.setName("btnSD"); // NOI18N

        btnINC.setAction(actionMap.get("Regra_INC")); // NOI18N
        btnINC.setText(resourceMap.getString("btnINC.text")); // NOI18N
        btnINC.setToolTipText(resourceMap.getString("btnINC.toolTipText")); // NOI18N
        btnINC.setName("btnINC"); // NOI18N

        btnEXP.setAction(actionMap.get("Regra_EXP")); // NOI18N
        btnEXP.setText(resourceMap.getString("btnEXP.text")); // NOI18N
        btnEXP.setToolTipText(resourceMap.getString("btnEXP.toolTipText")); // NOI18N
        btnEXP.setName("btnEXP"); // NOI18N

        btnDC.setAction(actionMap.get("Regra_DC")); // NOI18N
        btnDC.setText(resourceMap.getString("btnDC.text")); // NOI18N
        btnDC.setToolTipText(resourceMap.getString("btnDC.toolTipText")); // NOI18N
        btnDC.setName("btnDC"); // NOI18N

        jLabel5.setFont(resourceMap.getFont("jLabel11.font")); // NOI18N
        jLabel5.setText(resourceMap.getString("jLabel5.text")); // NOI18N
        jLabel5.setName("jLabel5"); // NOI18N

        jLabel12.setFont(resourceMap.getFont("jLabel11.font")); // NOI18N
        jLabel12.setText(resourceMap.getString("jLabel12.text")); // NOI18N
        jLabel12.setName("jLabel12"); // NOI18N

        jLabel13.setFont(resourceMap.getFont("jLabel11.font")); // NOI18N
        jLabel13.setText(resourceMap.getString("jLabel13.text")); // NOI18N
        jLabel13.setName("jLabel13"); // NOI18N

        jLabel14.setFont(resourceMap.getFont("jLabel11.font")); // NOI18N
        jLabel14.setText(resourceMap.getString("jLabel14.text")); // NOI18N
        jLabel14.setName("jLabel14"); // NOI18N

        jLabel15.setFont(resourceMap.getFont("jLabel11.font")); // NOI18N
        jLabel15.setText(resourceMap.getString("jLabel15.text")); // NOI18N
        jLabel15.setName("jLabel15"); // NOI18N

        jLabel16.setFont(resourceMap.getFont("jLabel11.font")); // NOI18N
        jLabel16.setText(resourceMap.getString("jLabel16.text")); // NOI18N
        jLabel16.setName("jLabel16"); // NOI18N

        jSeparator3.setName("jSeparator3"); // NOI18N

        btnDesfazer.setAction(actionMap.get("Desfazer")); // NOI18N
        btnDesfazer.setText(resourceMap.getString("btnDesfazer.text")); // NOI18N
        btnDesfazer.setToolTipText(resourceMap.getString("btnDesfazer.toolTipText")); // NOI18N
        btnDesfazer.setName("btnDesfazer"); // NOI18N

        btnRefazer.setAction(actionMap.get("Refazer")); // NOI18N
        btnRefazer.setText(resourceMap.getString("btnRefazer.text")); // NOI18N
        btnRefazer.setToolTipText(resourceMap.getString("btnRefazer.toolTipText")); // NOI18N
        btnRefazer.setName("btnRefazer"); // NOI18N

        btnLimpar.setAction(actionMap.get("Limpar")); // NOI18N
        btnLimpar.setText(resourceMap.getString("btnLimpar.text")); // NOI18N
        btnLimpar.setToolTipText(resourceMap.getString("btnLimpar.toolTipText")); // NOI18N
        btnLimpar.setName("btnLimpar"); // NOI18N

        btnMaiorLetra.setAction(actionMap.get("aumentaLetra")); // NOI18N
        btnMaiorLetra.setText(resourceMap.getString("btnMaiorLetra.text")); // NOI18N
        btnMaiorLetra.setToolTipText(resourceMap.getString("btnMaiorLetra.toolTipText")); // NOI18N
        btnMaiorLetra.setName("btnMaiorLetra"); // NOI18N

        btnMenorLetra.setAction(actionMap.get("diminuiLetra")); // NOI18N
        btnMenorLetra.setText(resourceMap.getString("btnMenorLetra.text")); // NOI18N
        btnMenorLetra.setToolTipText(resourceMap.getString("btnMenorLetra.toolTipText")); // NOI18N
        btnMenorLetra.setName("btnMenorLetra"); // NOI18N

        jSeparator2.setName("jSeparator2"); // NOI18N

        jButton11.setAction(actionMap.get("adicionaHip")); // NOI18N
        jButton11.setText(resourceMap.getString("jButton11.text")); // NOI18N
        jButton11.setToolTipText(resourceMap.getString("jButton11.toolTipText")); // NOI18N
        jButton11.setName("jButton11"); // NOI18N

        jButton13.setAction(actionMap.get("mostraHip")); // NOI18N
        jButton13.setText(resourceMap.getString("jButton13.text")); // NOI18N
        jButton13.setToolTipText(resourceMap.getString("jButton13.toolTipText")); // NOI18N
        jButton13.setName("jButton13"); // NOI18N

        jButton3.setAction(actionMap.get("popupAjuda")); // NOI18N
        jButton3.setText(resourceMap.getString("jButton3.text")); // NOI18N
        jButton3.setToolTipText(resourceMap.getString("jButton3.toolTipText")); // NOI18N
        jButton3.setName("jButton3"); // NOI18N

        labelIsLogado.setFont(resourceMap.getFont("labelIsLogado.font")); // NOI18N
        labelIsLogado.setText(resourceMap.getString("labelIsLogado.text")); // NOI18N
        labelIsLogado.setName("labelIsLogado"); // NOI18N

        btnLogar.setAction(actionMap.get("realizaLoginLogoff")); // NOI18N
        btnLogar.setText(resourceMap.getString("btnLogar.text")); // NOI18N
        btnLogar.setToolTipText(resourceMap.getString("btnLogar.toolTipText")); // NOI18N
        btnLogar.setName("btnLogar"); // NOI18N

        jLabel6.setFont(resourceMap.getFont("jLabel6.font")); // NOI18N
        jLabel6.setText(resourceMap.getString("jLabel6.text")); // NOI18N
        jLabel6.setName("jLabel6"); // NOI18N

        jLabel17.setFont(resourceMap.getFont("jLabel17.font")); // NOI18N
        jLabel17.setText(resourceMap.getString("jLabel17.text")); // NOI18N
        jLabel17.setName("jLabel17"); // NOI18N

        jLabel18.setFont(resourceMap.getFont("jLabel18.font")); // NOI18N
        jLabel18.setText(resourceMap.getString("jLabel18.text")); // NOI18N
        jLabel18.setName("jLabel18"); // NOI18N

        jLabel19.setFont(resourceMap.getFont("jLabel19.font")); // NOI18N
        jLabel19.setText(resourceMap.getString("jLabel19.text")); // NOI18N
        jLabel19.setName("jLabel19"); // NOI18N

        jLabel20.setFont(resourceMap.getFont("jLabel20.font")); // NOI18N
        jLabel20.setText(resourceMap.getString("jLabel20.text")); // NOI18N
        jLabel20.setName("jLabel20"); // NOI18N

        jLabel21.setFont(resourceMap.getFont("jLabel21.font")); // NOI18N
        jLabel21.setText(resourceMap.getString("jLabel21.text")); // NOI18N
        jLabel21.setName("jLabel21"); // NOI18N

        jLabel7.setFont(resourceMap.getFont("jLabel7.font")); // NOI18N
        jLabel7.setText(resourceMap.getString("jLabel7.text")); // NOI18N
        jLabel7.setName("jLabel7"); // NOI18N

        jLabel22.setFont(resourceMap.getFont("jLabel22.font")); // NOI18N
        jLabel22.setText(resourceMap.getString("jLabel22.text")); // NOI18N
        jLabel22.setName("jLabel22"); // NOI18N

        javax.swing.GroupLayout pnlRegrasLayout = new javax.swing.GroupLayout(pnlRegras);
        pnlRegras.setLayout(pnlRegrasLayout);
        pnlRegrasLayout.setHorizontalGroup(
            pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(pnlRegrasLayout.createSequentialGroup()
                .addContainerGap()
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                    .addComponent(jLabel2)
                    .addComponent(jLabel3)
                    .addGroup(pnlRegrasLayout.createSequentialGroup()
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.TRAILING, false)
                            .addComponent(btnRAA, javax.swing.GroupLayout.Alignment.LEADING, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnIEQ, javax.swing.GroupLayout.Alignment.LEADING, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnCJ, javax.swing.GroupLayout.Alignment.LEADING, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING, false)
                            .addComponent(btnDN, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnSP, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnEEQ, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING, false)
                            .addComponent(btnPC, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnAD, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING, false)
                            .addComponent(btnMP, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnEDJ, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)))
                    .addGroup(pnlRegrasLayout.createSequentialGroup()
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.TRAILING, false)
                            .addComponent(btnMT, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnEXP, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING, false)
                            .addComponent(btnINC, javax.swing.GroupLayout.Alignment.TRAILING, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnSH, javax.swing.GroupLayout.Alignment.TRAILING, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                        .addGap(10, 10, 10)
                        .addComponent(btnSD)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.UNRELATED)
                        .addComponent(btnDC))
                    .addGroup(pnlRegrasLayout.createSequentialGroup()
                        .addComponent(labelIsLogado)
                        .addGap(18, 18, 18)
                        .addComponent(btnLogar))
                    .addComponent(jLabel7)
                    .addGroup(pnlRegrasLayout.createSequentialGroup()
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                            .addComponent(jLabel6)
                            .addComponent(jLabel21)
                            .addComponent(jLabel20)
                            .addComponent(jLabel19)
                            .addComponent(jLabel18)
                            .addComponent(jLabel17))
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.UNRELATED)
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                            .addComponent(jLabel15)
                            .addComponent(jLabel14)
                            .addComponent(jLabel13)
                            .addComponent(jLabel12)
                            .addComponent(jLabel5)
                            .addComponent(jLabel16)))
                    .addComponent(jSeparator3, javax.swing.GroupLayout.DEFAULT_SIZE, 258, Short.MAX_VALUE)
                    .addComponent(jSeparator2, javax.swing.GroupLayout.DEFAULT_SIZE, 258, Short.MAX_VALUE)
                    .addGroup(pnlRegrasLayout.createSequentialGroup()
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.TRAILING)
                            .addComponent(btnLimpar, javax.swing.GroupLayout.DEFAULT_SIZE, 98, Short.MAX_VALUE)
                            .addComponent(btnDesfazer, javax.swing.GroupLayout.DEFAULT_SIZE, 98, Short.MAX_VALUE)
                            .addComponent(jButton11, javax.swing.GroupLayout.Alignment.LEADING, javax.swing.GroupLayout.DEFAULT_SIZE, 98, Short.MAX_VALUE))
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING, false)
                            .addComponent(jButton3, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnRefazer, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(jButton13, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING, false)
                            .addComponent(btnMenorLetra, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                            .addComponent(btnMaiorLetra, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                        .addContainerGap(12, Short.MAX_VALUE))
                    .addGroup(pnlRegrasLayout.createSequentialGroup()
                        .addComponent(jLabel22)
                        .addContainerGap(95, Short.MAX_VALUE))))
        );
        pnlRegrasLayout.setVerticalGroup(
            pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(pnlRegrasLayout.createSequentialGroup()
                .addComponent(jLabel2)
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(btnRAA)
                    .addComponent(btnDN)
                    .addComponent(btnPC)
                    .addComponent(btnMP))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(btnCJ)
                    .addComponent(btnSP)
                    .addComponent(btnAD)
                    .addComponent(btnEDJ))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(btnIEQ)
                    .addComponent(btnEEQ))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addComponent(jLabel3)
                .addGap(4, 4, 4)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(btnMT, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                    .addComponent(btnSD, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                    .addComponent(btnDC)
                    .addComponent(btnSH, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(btnEXP)
                    .addComponent(btnINC))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.UNRELATED)
                .addComponent(jSeparator3, javax.swing.GroupLayout.PREFERRED_SIZE, 9, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(btnDesfazer, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                    .addComponent(btnRefazer, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                    .addComponent(btnMaiorLetra, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(jButton11)
                    .addComponent(jButton13)
                    .addComponent(btnMenorLetra, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(btnLimpar, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                    .addComponent(jButton3))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                    .addComponent(labelIsLogado, javax.swing.GroupLayout.PREFERRED_SIZE, 20, javax.swing.GroupLayout.PREFERRED_SIZE)
                    .addComponent(btnLogar))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addComponent(jSeparator2, javax.swing.GroupLayout.PREFERRED_SIZE, 10, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addComponent(jLabel7)
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(pnlRegrasLayout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                    .addGroup(pnlRegrasLayout.createSequentialGroup()
                        .addComponent(jLabel6)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel17)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel18)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel19)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel20)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel21))
                    .addGroup(pnlRegrasLayout.createSequentialGroup()
                        .addComponent(jLabel5)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel12)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel13)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel14)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel15)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jLabel16)))
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addComponent(jLabel22)
                .addGap(32, 32, 32))
        );

        jSeparator1.setName("jSeparator1"); // NOI18N

        jComboBox1.setName("jComboBox1"); // NOI18N

        jComboBox2.setAction(actionMap.get("setComboBox1")); // NOI18N
        jComboBox2.setName("jComboBox2"); // NOI18N
        jComboBox2.addActionListener(new java.awt.event.ActionListener() {
            public void actionPerformed(java.awt.event.ActionEvent evt) {
                jComboBox2ActionPerformed(evt);
            }
        });

        jScrollPane2.setAutoscrolls(true);
        jScrollPane2.setName("jScrollPane2"); // NOI18N

        lstMensagem.setBackground(resourceMap.getColor("lstMensagem.background")); // NOI18N
        lstMensagem.setFont(resourceMap.getFont("lstMensagem.font")); // NOI18N
        lstMensagem.setName("lstMensagem"); // NOI18N
        jScrollPane2.setViewportView(lstMensagem);

        jSplitPane1.setDividerLocation(100);
        jSplitPane1.setEnabled(false);
        jSplitPane1.setName("jSplitPane1"); // NOI18N

        jScrollPane1.setAutoscrolls(true);
        jScrollPane1.setName("jScrollPane1"); // NOI18N
        jScrollPane1.setPreferredSize(new java.awt.Dimension(240, 130));

        lstTeorema.setFont(resourceMap.getFont("lstTeorema.font")); // NOI18N
        lstTeorema.setName("lstTeorema"); // NOI18N
        lstTeorema.addMouseListener(new java.awt.event.MouseAdapter() {
            public void mouseClicked(java.awt.event.MouseEvent evt) {
                lstTeoremaMouseClicked(evt);
            }
        });
        jScrollPane1.setViewportView(lstTeorema);

        jSplitPane1.setLeftComponent(jScrollPane1);

        jScrollPane3.setName("jScrollPane3"); // NOI18N

        lstProvador.setFont(resourceMap.getFont("lstProvador.font")); // NOI18N
        lstProvador.setEnabled(false);
        lstProvador.setName("lstProvador"); // NOI18N
        jScrollPane3.setViewportView(lstProvador);

        jSplitPane1.setRightComponent(jScrollPane3);

        txtArgumento.setText(resourceMap.getString("txtArgumento.text")); // NOI18N
        txtArgumento.setName("txtArgumento"); // NOI18N

        jLabel8.setFont(resourceMap.getFont("jLabel8.font")); // NOI18N
        jLabel8.setText(resourceMap.getString("jLabel8.text")); // NOI18N
        jLabel8.setName("jLabel8"); // NOI18N

        javax.swing.GroupLayout layout = new javax.swing.GroupLayout(this);
        this.setLayout(layout);
        layout.setHorizontalGroup(
            layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(layout.createSequentialGroup()
                .addContainerGap()
                .addComponent(pnlRegras, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                .addGroup(layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                    .addGroup(layout.createSequentialGroup()
                        .addGroup(layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                            .addComponent(jLabel8)
                            .addComponent(jLabel1, javax.swing.GroupLayout.PREFERRED_SIZE, 85, javax.swing.GroupLayout.PREFERRED_SIZE))
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.UNRELATED)
                        .addComponent(jComboBox2, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.UNRELATED)
                        .addComponent(jComboBox1, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(txtArgumento, javax.swing.GroupLayout.PREFERRED_SIZE, 160, javax.swing.GroupLayout.PREFERRED_SIZE)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(btnIniciar))
                    .addComponent(jScrollPane2, javax.swing.GroupLayout.DEFAULT_SIZE, 532, Short.MAX_VALUE)
                    .addComponent(jSplitPane1, javax.swing.GroupLayout.Alignment.TRAILING, javax.swing.GroupLayout.DEFAULT_SIZE, 532, Short.MAX_VALUE))
                .addContainerGap())
        );
        layout.setVerticalGroup(
            layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGroup(javax.swing.GroupLayout.Alignment.TRAILING, layout.createSequentialGroup()
                .addContainerGap()
                .addGroup(layout.createParallelGroup(javax.swing.GroupLayout.Alignment.TRAILING)
                    .addComponent(pnlRegras, javax.swing.GroupLayout.Alignment.LEADING, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, Short.MAX_VALUE)
                    .addGroup(layout.createSequentialGroup()
                        .addGroup(layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
                            .addGroup(layout.createSequentialGroup()
                                .addComponent(jLabel1, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                                .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                                .addComponent(jLabel8, javax.swing.GroupLayout.PREFERRED_SIZE, 17, javax.swing.GroupLayout.PREFERRED_SIZE))
                            .addGroup(layout.createParallelGroup(javax.swing.GroupLayout.Alignment.BASELINE)
                                .addComponent(jComboBox2, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                                .addComponent(jComboBox1, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                                .addComponent(txtArgumento, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)
                                .addComponent(btnIniciar, javax.swing.GroupLayout.PREFERRED_SIZE, 37, javax.swing.GroupLayout.PREFERRED_SIZE)))
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.RELATED)
                        .addComponent(jSplitPane1, javax.swing.GroupLayout.DEFAULT_SIZE, 378, Short.MAX_VALUE)
                        .addPreferredGap(javax.swing.LayoutStyle.ComponentPlacement.UNRELATED)
                        .addComponent(jScrollPane2, javax.swing.GroupLayout.PREFERRED_SIZE, javax.swing.GroupLayout.DEFAULT_SIZE, javax.swing.GroupLayout.PREFERRED_SIZE)))
                .addContainerGap())
        );

        jLabel1.getAccessibleContext().setAccessibleName(resourceMap.getString("jLabel1.AccessibleContext.accessibleName")); // NOI18N
    }// </editor-fold>//GEN-END:initComponents

    private void lstTeoremaMouseClicked(java.awt.event.MouseEvent evt) {//GEN-FIRST:event_lstTeoremaMouseClicked
        int pos = lstTeorema.getSelectedIndex();
        if (pos > 0) {
            if (Teorema[pos] != null) {
                if (!Teorema[pos].isUsable()) {
                    this.escreveParaUsuario("Linha finalizada");
                } else if (carregar) {
                    //Seta posiçao
                    if (pos1 == 0 && pos2 != pos) {
                        pos1 = pos;
                        if (pos1 <= indice) {
                            if (lastbtn == 5) {
                                Regra_EEQ();
                            } else if (lastbtn == 2) {
                                Regra_AD();
                            } else if (lastbtn == 6) {
                                Regra_SP();
                            } else if (lastbtn == 10) {
                                Regra_DN();
                            } else if (lastbtn == 16) {
                                Regra_EXP();
                            } else {
                                Teorema[pos1].selected();
                            }
                        } else {
                            pos1 = 0;
                        }
                    } else if (pos1 == pos) {
                        Teorema[pos1].unselect();
                        pos1 = 0;
                    } else if (pos2 == 0) {
                        pos2 = pos;
                        if (pos2 <= indice) {
                            if (lastbtn == 1) {
                                Regra_MP();
                            } else if (lastbtn == 3) {
                                Regra_CJ();
                            } else if (lastbtn == 4) {
                                Regra_IEQ();
                            } else if (lastbtn == 11) {
                                Regra_MT();
                            } else if (lastbtn == 12) {
                                Regra_SH();
                            } else if (lastbtn == 13) {
                                Regra_SD();
                            } else if (lastbtn == 14) {
                                Regra_INC();
                            } else {
                                Teorema[pos2].selected();
                            }
                        } else {
                            pos2 = 0;
                        }
                    } else if (pos2 == pos) {
                        Teorema[pos2].unselect();
                        pos2 = 0;
                    } else if (pos3 == 0) {
                        pos3 = pos;
                        if (pos3 <= indice) {
                            if (lastbtn == 7) {
                                Regra_EDJ();
                            } else if (lastbtn == 15) {
                                Regra_DC();
                            }
                        } else {
                            pos3 = 0;
                        }
                    }
                    lstTeorema.clearSelection(); //Limpa lista
                    lstTeorema.setListData(Teorema); //Carrega lista com os novos dados do Teorema
                }
            }
        }
    }//GEN-LAST:event_lstTeoremaMouseClicked

    private void jComboBox2ActionPerformed(java.awt.event.ActionEvent evt) {//GEN-FIRST:event_jComboBox2ActionPerformed
        // TODO add your handling code here:
        btnIniciar.setVisible(true);
        btnIniciar.setEnabled(true);
        nivel = jComboBox2.getSelectedItem().toString();
        if (nivel.equalsIgnoreCase("Inserir argumento")) {
            txtArgumento.setVisible(true);
            txtArgumento.setText("");
            jComboBox1.setVisible(false);
        } else {
            txtArgumento.setVisible(false);
            jComboBox1.setVisible(true);
            jComboBox1.setEnabled(true);
            jComboBox1.removeAllItems();
            try {
                nivel = jComboBox2.getSelectedItem().toString();
                InputStream is = this.getClass().getResourceAsStream("resources/Exercicios/" + nivel);
                BufferedReader br = new BufferedReader(new InputStreamReader(is));
                String temp = br.readLine();
                while (temp != null) {
                    jComboBox1.addItem(temp);
                    temp = br.readLine();
                }
                is.close();
                br.close();
            } catch (IOException ex) {
                Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE, null, ex);
            }
        }
        jLabel1.updateUI();
    }//GEN-LAST:event_jComboBox2ActionPerformed

    @Action
    public void Iniciar() {
        this.Limpar();
        lstTeorema.setEnabled(true);
        btnDesfazer.setEnabled(false);
        btnRefazer.setEnabled(false);
        this.setBotoes(false, true, true);
        if (nivel.equalsIgnoreCase("Inserir argumento")) {
            listaArgumento(txtArgumento.getText());
        } else {
            listaArgumento(jComboBox1.getSelectedItem().toString());
            if (jComboBox2.getSelectedItem().toString().equalsIgnoreCase("Lista_de_exercicio")
                    && jComboBox1.getSelectedIndex() < 4) {
                jButton13.setEnabled(false);
            }

            jComboBox1.removeAllItems();
        }
    }

    private void listaArgumento(String argumento) {
        if (!argumento.contains("|-")) {
            JOptionPane.showMessageDialog(null, "Erro no argumento");
            Limpar();
            return;
        }
        String aux[];
        resPCRAA = new String[50];

        lstTeorema.clearSelection();

        Teorema[0] = new Teorema("Teorema: " + argumento); //Carrega o teorema do usuário

        aux = argumento.split(",");//Separa o teorema para exibir as hipóteses

        total_hipoteses = aux.length; //Total de hipoteses. Controle para o desfazer

        if (aux[0].startsWith("|-")) {
            --total_hipoteses;
        }
        hipoteses = new Formula[total_hipoteses + 1];

        try {
            //Copia o teorema como hipótese             
            if (argumento.indexOf("|-") != 0) {
                for (int i = 0; i < aux.length; i++) {
                    if ((i + 1) != aux.length) {
                        hipoteses[i] = new Formula();
                        hipoteses[i].parse(aux[i]);
                        hipoteses[i] = eliminaParenteses(hipoteses[i], true);
                    } else {
                        hipoteses[i] = new Formula();
                        hipoteses[i].parse(aux[i].substring(0, aux[i].indexOf("|-")));
                        hipoteses[i] = eliminaParenteses(hipoteses[i], true);
                    }
                }
                indice = 0;  //Atualizar variavel auxiliar de controle
            } else {
                indice = 0;
                this.setBotoes(true, false, true);
            }

            formataArgumento();
            lstTeorema.setListData(Teorema); //Carrega lista com os novos dados do Teorema

            TeoremaAux = Teorema.clone(); //Atualiza a lista auxiliar do teorema

            indiceoriginal = aux.length;  //Atualizar variavel auxiliar de controle

            comunicaServidor("novo_argumento", "Novo Argumento");

        } catch (ParserException ex) {
            JOptionPane.showMessageDialog(null, "Erro no argumento");
            Limpar();
        } catch (ScannerException ex) {
            JOptionPane.showMessageDialog(null, "Erro no argumento");
            Limpar();
        }


    }

    @Action
    public void aumentaLetra() {
        Font font = lstTeorema.getFont().deriveFont(lstTeorema.getFont().getSize2D() + 1);
        lstTeorema.setFont(font);
        lstProvador.setFont(font);
        organiza();
    }

    @Action
    public void diminuiLetra() {
        Font font = lstTeorema.getFont().deriveFont(lstTeorema.getFont().getSize2D() - 1);
        lstTeorema.setFont(font);
        lstProvador.setFont(font);
        organiza();
    }

    @Action
    public void adicionaHip() {
        String aux = JOptionPane.showInputDialog(null, "Digite a Hipótese");
        Formula f = new Formula();
        boolean temp = false;//assinala se a hipótese está correta.
        if (aux != null && !aux.equalsIgnoreCase("")) {
            try {
                f.parse(aux);
                for (int x = 0; x < hipoteses.length; ++x) {
                    if (hipoteses[x] != null) {
                        if (f.equalsTo(hipoteses[x])) {
                            temp = true;
                            Teorema[++indice] = new Linha(f, "", "HIP ", 0, indice);
                            for (int y = x; y < hipoteses.length - 1; ++y) {
                                hipoteses[y] = hipoteses[y + 1];
                            }
                        }
                    }
                }
                if (!temp) {
                    this.escreveParaUsuario("Hipótese incorreta.");
                    comunicaServidor("diag_hipotese", "erro hipotese");
                } else {
                    this.escreveParaUsuario("Hipótese inserida com sucesso.");
                    comunicaServidor("diag_hipotese", "hipotese informada");
                }
                organiza();
                if (hipoteses[0] == null) {
                    this.escreveParaUsuario("Todas as hipóteses foram inseridas corretamente.\n");
                    this.setBotoes(true, false, true);
                }
            } catch (ScannerException ex) {
                JOptionPane.showMessageDialog(null, "Erro na fórmula.");
            } catch (ParserException ex) {
                JOptionPane.showMessageDialog(null, "Erro na fórmula.");
            }
        }
    }

    @Action
    public void mostraHip() {
        if (hipoteses[0] != null) {
            for (int x = 0; x < hipoteses.length; ++x) {
                if (hipoteses[x] != null) {
                    Teorema[++indice] = new Linha(hipoteses[x], "", "HIP ", 0, indice);
                }
            }
            for (int y = 0; y < hipoteses.length - 1; ++y) {
                hipoteses[y] = null;
            }
            this.setBotoes(true, false, true);
        }
        organiza();
    }

    private void terminaPCRAA() {
        int aux;
        for (int x = indice - 1; x > 0; --x) {
            aux = Teorema[x].getQtPCRAA();
            if (aux == qtPCRAA + 1) {
                Teorema[x].setUsable(false);
            } else if (aux == qtPCRAA) {
                return;
            }
        }
    }

    private void ReativaPCRAA() {
        int aux;
        for (int x = indice; x > 0; --x) {
            aux = Teorema[x].getQtPCRAA();
            if (aux == qtPCRAA + 1) {
                Teorema[x].setUsable(true);
            } else if (aux == qtPCRAA) {
                return;
            }
        }
    }

    private String getDate() {
        String date = Calendar.getInstance().get(Calendar.HOUR_OF_DAY) + ":";
        date += Calendar.getInstance().get(Calendar.MINUTE) + ":";
        date += Calendar.getInstance().get(Calendar.SECOND);
        return date;
    }

    private void testaRegra() {
        if (!regraCorreta) {
            this.testaQtErros();
            this.escreveParaUsuario("Regra incorreta");
            comunicaServidor("diag_prova", "erro regra-" + regras[lastbtn-1]);
        } else {
            qtErrosRegras[lastbtn - 1] = 0;
            regraCorreta = false;
            btnDesfazer.setEnabled(true);
            btnRefazer.setEnabled(false);
            this.escreveParaUsuario("Regra aplicada com sucesso ");
            comunicaServidor("diag_prova", "regra aplicada");
        }
    }

    private void comunicaServidor(String tipo, String tipo2) {
        if (WS2FIPAGateway.getUsername() != null) {
            String msg = tipo + "(" + '"' + "PC - " + this.nivel + '"' + "," + '"' + this.argumentoFormatado + '"' + "," + '"';
            if (indice > 0) {
                msg += this.formataProva();
            }
            msg += '"' + "," + '"' + tipo2 + '"' + "," + WS2FIPAGateway.getUsername() + ")";
            WS2FIPAGateway.sendMessageAsync(msg, this);
        }
    }

    private void formataArgumento() {
        argumentoFormatado = "[";
        for (int x = 0; x < total_hipoteses; ++x) {
            argumentoFormatado += hipoteses[x].display() + ", ";
        }
        if (total_hipoteses > 0) {
            argumentoFormatado = argumentoFormatado.substring(0, argumentoFormatado.length() - 2);
        }
        argumentoFormatado += " ] :-- " + Teorema[0].getFormula().display() + ".";
    }

    private String formataProva() {
        String prova = '"' + "";
        for (int x = 1; x < indice + 1; ++x) {
            prova += Teorema[x].formata() + "\n";
        }
        prova = prova.substring(0, prova.lastIndexOf("\n")) + '"';
        return prova;
    }

    @Action
    public void popupAjuda() {
        ajudaDica.setEnabled(WS2FIPAGateway.getUsername() != null);
        jFrame4.setVisible(true);
        jFrame4.setBounds(540, 250, 263, 200);
    }

    @Action
    public void okAjuda() {
        if (ajudaManual.isSelected()) {
            Principal.AcaoManual();
            /* } else if (ajudaRegras.isSelected()) {
            if (qtAjuda == 0) {
            qtAjuda = 1;
            }*/
        } else if (ajudaExemplos.isSelected()) {
            Principal.AcaoExemploTeoremas();
            if (qtAjuda < 1) {
                qtAjuda = 1;
            }
        } else if (ajudaDica.isSelected()) {
            if (qtAjuda == 0) {
                Principal.AcaoExemploTeoremas();
            } else {
                if (indice < total_hipoteses) {
                    String msg = "Próxima hipótese: " + hipoteses[0].display();
                    this.escreveParaUsuario(msg);
                } else {
                    comunicaServidor("solic_ajuda", "ajuda solicitada");
                }
            }
            ++qtAjuda;
        }
        buttonGroup1.clearSelection();
        jFrame4.setVisible(false);
    }

    public void informaLogado() {
        if (WS2FIPAGateway.getUsername() == null) { //Testa se o usuario está logado
            labelIsLogado.setText("Você não está logado:");
            btnLogar.setText("LOGIN");
            btnLogar.setToolTipText("Clique aqui para fazer login");
        } else {
            labelIsLogado.setText("Você está logado(" + WS2FIPAGateway.getUsername() + "):");
            btnLogar.setText("LOGOFF");
            btnLogar.setToolTipText("Clique aqui para fazer logoff");
        }
    }

    @Action
    public void realizaLoginLogoff() {
        if (WS2FIPAGateway.getUsername() == null) {
            LoginDialog n = new LoginDialog(HeraclitoApp.getApplication().getMainFrame(), true);
            n.setVisible(true);
            if (n.getBtnPressed() == 0) {//Se o botão pressionado for cancelar, retorna.
                return;
            }
            Principal.getBV().setUsernamePassword(n.getReturnStatus());
        } else {
            resolucao = null;
        }
        Principal.getBV().AcaoLoginLogoff();
    }

    public void escreveParaUsuario(String msg) {
        msgAgent.add(this.getDate() + " - " + msg);
        msgAgent.add(" ");
        msgAgent.add(" ");
        lstMensagem.setListData(msgAgent.toArray());
        int lastIndex = lstMensagem.getModel().getSize() - 1;
        if (lastIndex >= 0) {
            lstMensagem.ensureIndexIsVisible(lastIndex);
        }
    }

    public void ofereceExemplos(String msg) {
        int escolha = JOptionPane.showConfirmDialog(null, msg, "", JOptionPane.YES_NO_OPTION);
        if (escolha == JOptionPane.YES_OPTION) {
            Principal.AcaoExemploTeoremas();
        }
    }

    public void formataResolucaoProvador(String msg) {
        String aux[] = msg.replace('"' + "", "").split(";");
        String aux2[] = new String[5];
        int aux3 = 0;
        String msgAux;
        resolucao = new String[aux.length + 1];
        resolucao[0] = "Resolução do provador:";
        for (int x = 0; x < aux.length; ++x) {
            aux2[0] = aux[x].substring(0, 6);
            aux2[1] = aux[x].substring(6, 10);
            aux2[2] = aux[x].substring(10, 35);
            aux2[3] = aux[x].substring(35, 45);
            aux2[4] = aux[x].substring(45);
            msgAux = aux2[0].substring(0, aux[x].indexOf("."));
            int tam = 4 - msgAux.length();
            for (int y = 0; y < tam; ++y) {
                msgAux += " ";
            }
            aux3 = Integer.parseInt(aux2[1].substring(0, aux2[1].indexOf(".")));
            for (int z = 0; z < aux3; ++z) {
                msgAux += "| ";
            }
            msgAux += aux2[2];
            tam = 39 - msgAux.length();
            for (int y = 0; y < tam; ++y) {
                msgAux += " ";
            }
            msgAux += aux2[3].trim() + " " + aux2[4].replace("[", "").replace("]", "");
            resolucao[x + 1] = msgAux.replace(".", "").replace("'", "").toUpperCase().replaceAll("V", "v");
        }
    }

    private void testaQtErros() {
        ++qtErrosSeguidos;
        if (qtErrosSeguidos == 3) {
        }
        ++qtErrosRegras[lastbtn - 1];
        if (qtErrosRegras[lastbtn - 1] == 3) {
            qtErrosRegras[lastbtn - 1] = 0;
            //this.ofereceExemplos();
        }
    }
    // Variables declaration - do not modify//GEN-BEGIN:variables
    private javax.swing.JRadioButton ajudaDica;
    private javax.swing.JRadioButton ajudaExemplos;
    private javax.swing.JRadioButton ajudaManual;
    private javax.swing.JButton btnAD;
    private javax.swing.JButton btnAmbos;
    private javax.swing.JButton btnCJ;
    private javax.swing.JButton btnDC;
    private javax.swing.JButton btnDN;
    private javax.swing.JButton btnDesfazer;
    private javax.swing.JButton btnDireita;
    private javax.swing.JButton btnEDJ;
    private javax.swing.JButton btnEEQ;
    private javax.swing.JButton btnEXP;
    private javax.swing.JButton btnEsquerda;
    private javax.swing.JButton btnIEQ;
    private javax.swing.JButton btnINC;
    private javax.swing.JButton btnIniciar;
    private javax.swing.JButton btnLimpar;
    private javax.swing.JButton btnLogar;
    private javax.swing.JButton btnMP;
    private javax.swing.JButton btnMT;
    private javax.swing.JButton btnMaiorLetra;
    private javax.swing.JButton btnMenorLetra;
    private javax.swing.JButton btnOK;
    private javax.swing.JButton btnPC;
    private javax.swing.JButton btnRAA;
    private javax.swing.JButton btnRefazer;
    private javax.swing.JButton btnSD;
    private javax.swing.JButton btnSH;
    private javax.swing.JButton btnSP;
    private javax.swing.ButtonGroup buttonGroup1;
    private javax.swing.JButton jButton1;
    private javax.swing.JButton jButton11;
    private javax.swing.JButton jButton13;
    private javax.swing.JButton jButton2;
    private javax.swing.JButton jButton3;
    private javax.swing.JButton jButton4;
    private javax.swing.JButton jButton6;
    private javax.swing.JButton jButton7;
    private javax.swing.JButton jButton9;
    private javax.swing.JComboBox jComboBox1;
    private javax.swing.JComboBox jComboBox2;
    private javax.swing.JFileChooser jFileChooser1;
    private javax.swing.JFrame jFrame1;
    private javax.swing.JFrame jFrame2;
    private javax.swing.JFrame jFrame3;
    private javax.swing.JFrame jFrame4;
    private javax.swing.JFrame jFrame5;
    private javax.swing.JLabel jLabel1;
    private javax.swing.JLabel jLabel12;
    private javax.swing.JLabel jLabel13;
    private javax.swing.JLabel jLabel14;
    private javax.swing.JLabel jLabel15;
    private javax.swing.JLabel jLabel16;
    private javax.swing.JLabel jLabel17;
    private javax.swing.JLabel jLabel18;
    private javax.swing.JLabel jLabel19;
    private javax.swing.JLabel jLabel2;
    private javax.swing.JLabel jLabel20;
    private javax.swing.JLabel jLabel21;
    private javax.swing.JLabel jLabel22;
    private javax.swing.JLabel jLabel3;
    private javax.swing.JLabel jLabel38;
    private javax.swing.JLabel jLabel39;
    private javax.swing.JLabel jLabel4;
    private javax.swing.JLabel jLabel40;
    private javax.swing.JLabel jLabel41;
    private javax.swing.JLabel jLabel42;
    private javax.swing.JLabel jLabel5;
    private javax.swing.JLabel jLabel6;
    private javax.swing.JLabel jLabel7;
    private javax.swing.JLabel jLabel8;
    private javax.swing.JScrollPane jScrollPane1;
    private javax.swing.JScrollPane jScrollPane2;
    private javax.swing.JScrollPane jScrollPane3;
    private javax.swing.JSeparator jSeparator1;
    private javax.swing.JSeparator jSeparator2;
    private javax.swing.JSeparator jSeparator3;
    private javax.swing.JSplitPane jSplitPane1;
    private javax.swing.JTextField jTextField1;
    private javax.swing.JTextField jTextField2;
    private javax.swing.JLabel labelIsLogado;
    private javax.swing.JList lstMensagem;
    private javax.swing.JList lstProvador;
    private javax.swing.JList lstTeorema;
    private javax.swing.JPanel pnlRegras;
    private javax.swing.JTextField txtArgumento;
    // End of variables declaration//GEN-END:variables
}
